]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_unification/cicMetaSubst.ml
uniformed ppmetasenv to other pp* methods: substs are now passed _before_ the metasenv
[helm.git] / helm / ocaml / cic_unification / cicMetaSubst.ml
index 3b8e4ad221646ba6f0e949eb1250e2ba04e477bb..aea2a262526a20aaeea0caa6f4b2cdcb41d8c1f0 100644 (file)
@@ -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)