diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/command.ml | 3 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 13 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
3 files changed, 12 insertions, 6 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index 120f9590f2..a1a87d54e0 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -518,7 +518,8 @@ let check_param = function | CLocalDef (na, _, _) -> check_named na | CLocalAssum (nas, Default _, _) -> List.iter check_named nas | CLocalAssum (nas, Generalized _, _) -> () -| CLocalPattern _ -> assert false +| CLocalPattern (loc,_) -> + Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.") let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = check_all_names_different indl; diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 5298ef2e44..b2d48bb2f9 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -991,7 +991,7 @@ let is_not_printable onlyparse nonreversible = function (warn_non_reversible_notation (); true) else onlyparse -let find_precedence lev etyps symbols = +let find_precedence lev etyps symbols onlyprint = let first_symbol = let rec aux = function | Break _ :: t -> aux t @@ -1009,8 +1009,13 @@ let find_precedence lev etyps symbols = | None -> [],0 | Some (NonTerminal x) -> (try match List.assoc x etyps with - | ETConstr _ -> - user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") + | ETConstr _ -> + if onlyprint then + if Option.is_empty lev then + user_err Pp.(str "Explicit level needed in only-printing mode when the level of the leftmost non-terminal is given.") + else [],Option.get lev + else + user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") | ETName | ETBigint | ETReference -> begin match lev with | None -> @@ -1134,7 +1139,7 @@ let compute_syntax_data df modifiers = let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in let ntn_for_grammar = if need_squash then make_notation_key symbols_for_grammar else ntn_for_interp in if not onlyprint then check_rule_productivity symbols_for_grammar; - let msgs,n = find_precedence mods.level mods.etyps symbols in + let msgs,n = find_precedence mods.level mods.etyps symbols onlyprint in (* To globalize... *) let etyps = join_auxiliary_recursive_types recvars mods.etyps in let sy_typs, prec = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 83296cf58f..203d913db8 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1785,7 +1785,7 @@ let vernac_locate = let open Feedback in function (Constrextern.without_symbols pr_lglob_constr) ntn sc) | LocateLibrary qid -> print_located_library qid | LocateModule qid -> msg_notice (print_located_module qid) - | LocateTactic qid -> msg_notice (print_located_tactic qid) + | LocateOther (s, qid) -> msg_notice (print_located_other s qid) | LocateFile f -> msg_notice (locate_file f) let vernac_register id r = |