diff options
| -rw-r--r-- | translate/ppvernacnew.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 79ba46576c..de2f055996 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -1076,7 +1076,8 @@ let pr_vernac = function ["Refine"; "Inv"; "Equality"; "EAuto"; "AutoRewrite"; "EqDecide"; "Xml"; "Extraction"; "Tauto"; "Setoid_replace";"Elimdep"; "DatatypesSyntax"; "LogicSyntax"; "Logic_TypeSyntax"; - "SpecifSyntax"; "PeanoSyntax"; "TypeSyntax"; "PolyListSyntax"] -> + "SpecifSyntax"; "PeanoSyntax"; "TypeSyntax"; "PolyListSyntax"; + "Zsyntax";"zarith_aux"] -> warning ("Forgetting obsolete module "^(string_of_id r)); mt() | VernacImport (false,[Libnames.Ident (_,a)]) when |