diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-10 15:04:13 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-10 15:53:06 +0200 |
| commit | 0acaa906367c02c57a6d70dd5d19eaea884b7568 (patch) | |
| tree | 12cf860589f0d32db04610771752d6022a0c01d9 /vernac/metasyntax.ml | |
| parent | dfa99b152114271cf9fac4cab9d8663ac6ec078c (diff) | |
Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).
Diffstat (limited to 'vernac/metasyntax.ml')
| -rw-r--r-- | vernac/metasyntax.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index feeca6075..76958b05f 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -738,12 +738,12 @@ let cache_one_syntax_extension se = let prec = se.synext_level in let onlyprint = se.synext_notgram.notgram_onlyprinting in try - let oldprec = Notation.level_of_notation ntn in + let oldprec = Notation.level_of_notation ~onlyprint ntn in if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec; with Not_found -> if is_active_compat se.synext_compat then begin (* Reserve the notation level *) - Notation.declare_notation_level ntn prec; + Notation.declare_notation_level ntn prec ~onlyprint; (* Declare the parsing rule *) if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules; (* Declare the notation rule *) @@ -1274,7 +1274,7 @@ exception NoSyntaxRule let recover_notation_syntax ntn = try - let prec = Notation.level_of_notation ntn in + let prec = Notation.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in let pp_rule,_ = Notation.find_notation_printing_rule ntn in let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in let pa_rule = Notation.find_notation_parsing_rules ntn in |