diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-21 13:13:06 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-21 13:13:06 +0000 |
| commit | 6b68976978fc8b4e9589a35858bd5592347be635 (patch) | |
| tree | 63451122a67cd8db0016efb02f0a2330828c49c7 /translate/ppconstrnew.ml | |
| parent | 1e160525650bb03c286d78f061f73dcd865b0937 (diff) | |
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
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4045 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate/ppconstrnew.ml')
| -rw-r--r-- | translate/ppconstrnew.ml | 11 |
1 files changed, 10 insertions, 1 deletions
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")" |