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 3b8e4ad221646ba6f0e949eb1250e2ba04e477bb..aea2a262526a20aaeea0caa6f4b2cdcb41d8c1f0 100644 (file)
--- 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 a816d86b9cc8af9d333263a18b9a59e98927ae9d..7d78cec5cd9047210680839e5a2a9d5a89980f2d 100644 (file)
--- 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 f216b3c5c03429324561f49e8a89e770246063e1..e4b935089ebdb26c992b7db79b2afacefcbd93e3 100644 (file)
--- 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 dc7cd2721b91d02ea0bb8dd31aacf536312654de..8ae28448387aee48141c3382d3dce78883fa62fc 100644 (file)
--- 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