diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-29 14:12:21 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-29 14:12:21 +0000 |
| commit | 22b3af749027a819964a3639498a4ce53b34be01 (patch) | |
| tree | ff897c7a61eef4c556f584edcac3585dbe2efb7f /translate | |
| parent | 67787e6daeb7bf2fe59d5546969197ca9f87c2dc (diff) | |
Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3807 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index 2d86e00c9..eee2042a0 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -456,7 +456,19 @@ 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 pr_binders = pr_binders pr +let anonymize_binder na c = + if Options.do_translate() then + Constrextern.extern_rawconstr (Termops.vars_of_env (Global.env())) + (Reserve.anonymize_if_reserved na + (Constrintern.for_grammar + (Constrintern.interp_rawconstr Evd.empty (Global.env())) c)) + else c + +let pr_binders l = + prlist_with_sep sep + (fun (nal,t) -> prlist_with_sep sep + (fun (_,na as x) -> pr_oneb pr (anonymize_binder na t) x) nal) l + let pr_cases_pattern = pr_patt ltop let pr_pattern = pr_constr |