From 779151991397bb0824ec058cbccfed83af0f61a5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 4 Feb 2004 23:27:11 +0000 Subject: [PATCH] ppterm_in_context exported --- helm/ocaml/cic_unification/cicMetaSubst.mli | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli index 730afcd10..9fbe01946 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.mli +++ b/helm/ocaml/cic_unification/cicMetaSubst.mli @@ -58,10 +58,12 @@ val apply_subst_metasenv: substitution -> Cic.metasenv -> Cic.metasenv (** {2 Pretty printers} *) -val ppcontext: ?sep: string -> substitution -> Cic.context -> string -val ppmetasenv: ?sep: string -> Cic.metasenv -> substitution -> string val ppsubst: substitution -> string val ppterm: substitution -> Cic.term -> string +val ppcontext: ?sep: string -> substitution -> Cic.context -> string +val ppterm_in_context: + substitution -> Cic.term -> (Cic.name option) list -> string +val ppmetasenv: ?sep: string -> Cic.metasenv -> substitution -> string (* {2 Kernel wrappers} * From now on we recreate a kernel abstraction where substitutions are part of -- 2.39.2