diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-31 21:05:41 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-31 21:05:41 +0000 |
| commit | 5a3a8c0eecd82a32a6c20491ee2dc6022b8eab95 (patch) | |
| tree | f1ebbeef90718e0fa1d243775ef85e58ca6f499c /translate | |
| parent | 365960408f4c378f2f43e897ab102d2eeab8f6bd (diff) | |
Ajout VernacReserve et suppression des types re-inferables
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3820 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppvernacnew.ml | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 2ba13bb79..e6b306be2 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -220,8 +220,16 @@ let pr_type_option pr_c = function | CHole loc -> mt() | _ as c -> str":" ++ pr_c c +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_binder pr_c ty na = - match ty with + match anonymize_binder (snd na) ty with CHole _ -> pr_located pr_name na | _ -> hov 1 @@ -648,6 +656,10 @@ let rec pr_vernac = function | VernacDeclareImplicits (q,Some l) -> hov 1 (str"Implicits" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep int l ++ str"]") + | VernacReserve (idl,c) -> + hov 1 (str"Implicit Variable" ++ + str (if List.length idl > 1 then "s " else " ") ++ str "Type " ++ + prlist_with_sep spc pr_id idl ++ str " : " ++ pr_constr c) | VernacSetOpacity (fl,l) -> hov 1 ((if fl then str"Opaque" else str"Transparent") ++ spc() ++ prlist_with_sep sep pr_reference l) |