diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-10 08:03:26 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-10 08:03:26 +0000 |
| commit | 9a72107debe9027470c1cc93b869097b3201a967 (patch) | |
| tree | d4a8b1dab605f7984d7466072c2547fdd8c0f159 /translate | |
| parent | a10a0c02ad7698b778d52d3d0c6093111c24ac43 (diff) | |
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
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppvernacnew.ml | 16 |
1 files changed, 14 insertions, 2 deletions
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 |