From edb55a94fc5c0473e57f5a61c0c723194c2ff414 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 27 Sep 2016 17:15:10 +0200 Subject: Fix bug #4798: compat notations should not modify the parser. This is a quick fix. The Metasyntax module should be thoroughly revised in trunk, because it starts featuring a lot of spaghetti code and redundant data. --- printing/ppvernac.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 1d8dcabcc..503b29aaf 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -367,8 +367,8 @@ module Make | SetAssoc NonA -> keyword "no associativity" | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ | SetOnlyPrinting -> keyword "only printing" - | SetOnlyParsing Flags.Current -> keyword "only parsing" - | SetOnlyParsing v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") + | SetOnlyParsing -> keyword "only parsing" + | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") | SetFormat("text",s) -> keyword "format " ++ pr_located qs s | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s @@ -1002,13 +1002,13 @@ module Make ) | VernacHints (_, dbnames,h) -> return (pr_hints dbnames h pr_constr pr_constr_pattern_expr) - | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) -> + | VernacSyntacticDefinition (id,(ids,c),_,compat) -> return ( hov 2 (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ pr_syntax_modifiers - (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v])) + (match compat with None -> [] | Some v -> [SetCompatVersion v])) ) | VernacDeclareImplicits (q,[]) -> return ( -- cgit v1.2.3