From 9a72107debe9027470c1cc93b869097b3201a967 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 10 Oct 2003 08:03:26 +0000 Subject: Renommage en v8 de PolyList en List et List en MonoList git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4556 85f007b7-540e-0410-9357-904b9bb8a0f7 --- translate/ppvernacnew.ml | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) (limited to 'translate') diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index b04ff3efc..1e392b548 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -33,7 +33,19 @@ let pr_id id = pr_id (Constrextern.v7_to_v8_id id) let pr_ltac_id id = pr_id (id_of_ltac_v7_id id) -let pr_module = Libnames.pr_reference +let pr_module r = + let update_ref s = match r with + | Ident (loc,_) -> + Ident (loc,id_of_string s) + | Qualid (loc,qid) -> + Qualid (loc,make_qualid (fst (repr_qualid qid)) (id_of_string s)) in + let (_,dir,_) = + Library.locate_qualified_library (snd (qualid_of_reference r)) in + let r = match List.rev (List.map string_of_id (repr_dirpath dir)) with + | [ "Coq"; "Lists"; "List" ] -> update_ref "MonoList" + | [ "Coq"; "Lists"; "PolyList" ] -> update_ref "List" + | _ -> r in + Libnames.pr_reference r let pr_reference r = let loc = loc_of_reference r in @@ -1097,7 +1109,7 @@ let pr_vernac = function ["Refine"; "Inv"; "Equality"; "EAuto"; "AutoRewrite"; "EqDecide"; "Xml"; "Extraction"; "Tauto"; "Setoid_replace";"Elimdep"; "DatatypesSyntax"; "LogicSyntax"; "Logic_TypeSyntax"; - "SpecifSyntax"; "PeanoSyntax"; "TypeSyntax"] -> + "SpecifSyntax"; "PeanoSyntax"; "TypeSyntax"; "PolyListSyntax"] -> warning ("Forgetting obsolete module "^(string_of_id r)); mt() | VernacSyntax _ | VernacGrammar _ as x -> pr_vernac x -- cgit v1.2.3