From 0319dd1bc1f0b431945f9641a587fa52d6472ebc Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 15 Sep 2005 09:16:26 +0000 Subject: [PATCH] uniformed ppmetasenv to other pp* methods: substs are now passed _before_ the metasenv --- helm/ocaml/cic_unification/cicMetaSubst.ml | 4 ++-- helm/ocaml/cic_unification/cicMetaSubst.mli | 2 +- helm/ocaml/cic_unification/cicRefine.ml | 2 +- helm/ocaml/cic_unification/cicUnification.ml | 4 ++-- 4 files changed, 6 insertions(+), 6 deletions(-) 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 -- 2.39.2