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

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

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