diff options
| -rw-r--r-- | translate/ppvernacnew.ml | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index c7602c2b0f..42c518e5a9 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -629,7 +629,7 @@ let rec pr_vernac = function (match bl with | [] -> mt() | _ -> error "Statements with local binders no longer supported") - ++ str":" ++ spc() ++ pr_type c) + ++ str":" ++ spc() ++ pr_type (rename_bound_variables id c)) | VernacEndProof Admitted -> str"Admitted" | VernacEndProof (Proved (opac,o)) -> (match o with | None -> if opac then str"Qed" else str"Defined" @@ -1076,9 +1076,20 @@ let pr_vernac = function "Xml"; "Extraction"; "Tauto"; "Setoid_replace";"Elimdep"; "DatatypesSyntax"; "LogicSyntax"; "Logic_TypeSyntax"; "SpecifSyntax"; "PeanoSyntax"; "TypeSyntax"; "PolyListSyntax"; - "Zsyntax";"zarith_aux"] -> + "Zsyntax"] -> warning ("Forgetting obsolete module "^(string_of_id r)); mt() + | VernacRequire (exp,spe,[Ident(_,r)]) when + (* Renamed modules *) + List.mem (string_of_id r) ["zarith_aux";"fast_integer"] -> + warning ("Replacing obsolete module "^(string_of_id r)^" with ZArith"); + (str "Require" ++ pr_require_token exp ++ spc() ++ + (match spe with + | None -> mt() + | Some flag -> + (if flag then str"Specification" else str"Implementation") ++ + spc ()) ++ + str "ZArith.") | VernacImport (false,[Libnames.Ident (_,a)]) when (* Pour ceux qui ont utilisé la couche "Import *_scope" de compat *) let a = Names.string_of_id a in |