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

[helm.git] / helm / ocaml / cic_unification / cicUnification.ml

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