From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 15 Sep 2005 09:16:26 +0000 (+0000)
Subject: uniformed ppmetasenv to other pp* methods: substs are now passed _before_ the metasenv
X-Git-Tag: LAST_BEFORE_NEW~129
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0319dd1bc1f0b431945f9641a587fa52d6472ebc;p=helm.git

uniformed ppmetasenv to other pp* methods: substs are now passed _before_ the metasenv
---

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 3b8e4ad22..aea2a2625 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -334,7 +334,7 @@ let ppsubst subst =
 
 let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
 
-let ppmetasenv ?(sep = "\n") metasenv subst =
+let ppmetasenv ?(sep = "\n") subst metasenv =
   String.concat sep
     (List.map
       (fun (i, c, t) ->
@@ -886,5 +886,5 @@ let fpp_gen ppf s =
 
 let fppsubst ppf subst = fpp_gen ppf (ppsubst subst)
 let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term)
-let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv metasenv [])
+let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv)
 
diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli
index a816d86b9..7d78cec5c 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.mli
+++ b/helm/ocaml/cic_unification/cicMetaSubst.mli
@@ -67,7 +67,7 @@ val ppterm: Cic.substitution -> Cic.term -> string
 val ppcontext: ?sep: string -> Cic.substitution -> Cic.context -> string
 val ppterm_in_context:
  Cic.substitution -> Cic.term -> (Cic.name option) list -> string
-val ppmetasenv: ?sep: string -> Cic.metasenv -> Cic.substitution -> string
+val ppmetasenv: ?sep: string -> Cic.substitution -> Cic.metasenv -> string
 
 (** {2 Format-like pretty printers}
  * As above with prototypes suitable for toplevel/ocamldebug printers. No
diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index f216b3c5c..e4b935089 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -867,7 +867,7 @@ and type_of_aux' metasenv context t ugraph =
 	debug_print (Printf.sprintf "hetype=%s\nhetype'=%s\nmetasenv=%s\nsubst=%s"
 			 (CicPp.ppterm hetype)
 			 (CicPp.ppterm hetype')
-			 (CicMetaSubst.ppmetasenv metasenv [])
+                         (CicMetaSubst.ppmetasenv [] metasenv)
 			 (CicMetaSubst.ppsubst subst));
 	raise exn
 
diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index dc7cd2721..8ae284483 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -43,7 +43,7 @@ let type_of_aux' metasenv subst context term ugraph =
              (CicMetaSubst.ppterm subst term)
              (CicMetaSubst.ppterm [] term)
              (CicMetaSubst.ppcontext subst context)
-             (CicMetaSubst.ppmetasenv metasenv subst) 
+             (CicMetaSubst.ppmetasenv subst metasenv) 
              (CicMetaSubst.ppsubst subst) msg) in
         raise (AssertFailure msg);;
 
@@ -651,7 +651,7 @@ let fo_unif_subst subst context metasenv t1 t2 ugraph =
         CicPp.ppterm ty_t2
       with _ -> "MALFORMED")
       (CicMetaSubst.ppcontext subst context)
-      (CicMetaSubst.ppmetasenv metasenv subst)
+      (CicMetaSubst.ppmetasenv subst metasenv)
       (CicMetaSubst.ppsubst subst) msg 
   in
   try