From 6b68976978fc8b4e9589a35858bd5592347be635 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 21 May 2003 13:13:06 +0000 Subject: Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour les metavariables de patterns; réparation local défs récursive dans ltac MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4045 85f007b7-540e-0410-9357-904b9bb8a0f7 --- translate/ppconstrnew.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'translate/ppconstrnew.ml') diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 92feaa7de..a3b430c7d 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -527,6 +527,16 @@ let pr_lconstr_env env c = pr ltop (transf env c) let pr_constr c = pr_constr_env (Global.env()) c let pr_lconstr c = pr_lconstr_env (Global.env()) c +let transf_pattern env c = + if Options.do_translate() then + Constrextern.extern_rawconstr (Termops.vars_of_env env) + (Constrintern.for_grammar + (Constrintern.interp_rawconstr_gen false Evd.empty env [] None ([],[])) + c) + else c + +let pr_pattern c = pr lsimple (transf_pattern (Global.env()) c) + let pr_rawconstr_env env c = pr_constr (Constrextern.extern_rawconstr (Termops.vars_of_env env) c) let pr_lrawconstr_env env c = @@ -547,7 +557,6 @@ let pr_binders l = let pr_cases_pattern = pr_patt ltop -let pr_pattern = pr_constr let pr_occurrences prc (nl,c) = prlist (fun n -> int n ++ spc ()) nl ++ str"(" ++ prc c ++ str")" -- cgit v1.2.3