aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-03-22 14:33:22 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-03-22 14:36:14 +0100
commit8b73fd7c6ce423f8c8a2594e90200f2407795d52 (patch)
tree91db0f56763e6512016055a8dc47185f7317fe6b /vernac
parent6e0ca299c407125a8d65f54ab424bdae3667125e (diff)
parentcd87eac3757d8925ff4ba7dee85efadb195153a3 (diff)
Merge branch 'v8.6'
Diffstat (limited to 'vernac')
-rw-r--r--vernac/metasyntax.ml16
1 files changed, 10 insertions, 6 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 0aaf6afd7..7e98d114a 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -932,8 +932,8 @@ let find_precedence lev etyps symbols =
let first_symbol =
let rec aux = function
| Break _ :: t -> aux t
- | h :: t -> h
- | [] -> assert false (* rule is known to be productive *) in
+ | h :: t -> Some h
+ | [] -> None in
aux symbols in
let last_is_terminal () =
let rec aux b = function
@@ -943,7 +943,8 @@ let find_precedence lev etyps symbols =
| [] -> b in
aux false symbols in
match first_symbol with
- | NonTerminal x ->
+ | None -> [],0
+ | Some (NonTerminal x) ->
(try match List.assoc x etyps with
| ETConstr _ ->
error "The level of the leftmost non-terminal cannot be changed."
@@ -966,11 +967,11 @@ let find_precedence lev etyps symbols =
if Option.is_empty lev then
error "A left-recursive notation must have an explicit level."
else [],Option.get lev)
- | Terminal _ when last_is_terminal () ->
+ | Some (Terminal _) when last_is_terminal () ->
if Option.is_empty lev then
([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."], 0)
else [],Option.get lev
- | _ ->
+ | Some _ ->
if Option.is_empty lev then error "Cannot determine the level.";
[],Option.get lev
@@ -1049,6 +1050,9 @@ let compute_syntax_data df modifiers =
let open SynData in
let open NotationMods in
let mods = interp_modifiers modifiers in
+ let onlyprint = mods.only_printing in
+ let onlyparse = mods.only_parsing in
+ if onlyprint && onlyparse then error "A notation cannot be both 'only printing' and 'only parsing'.";
let assoc = Option.append mods.assoc (Some NonA) in
let toks = split_notation_string df in
let recvars,mainvars,symbols = analyze_notation_tokens toks in
@@ -1058,7 +1062,7 @@ let compute_syntax_data df modifiers =
let ntn_for_interp = make_notation_key symbols in
let symbols' = remove_curly_brackets symbols in
let ntn_for_grammar = make_notation_key symbols' in
- check_rule_productivity symbols';
+ if not onlyprint then check_rule_productivity symbols';
(* Misc *)
let need_squash = not (List.equal Notation.symbol_eq symbols symbols') in