Merge branch 'trunk' into located_switch

1 files changed, 8 insertions, 12 deletions

diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 1de4024fd1..4d7b0f9296 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -15,14 +15,13 @@ open Genarg
 open Extend
 open Pcoq
 open Egramml
-open Egramcoq
 open Vernacexpr
 open Libnames
 open Nameops
 
 type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
 | TacTerm of string
-| TacNonTerm of ('a * Names.Id.t) Loc.located
+| TacNonTerm of ('a * Names.Id.t option) Loc.located
 
 type raw_argument = string * string option
 type argument = Genarg.ArgT.any Extend.user_symbol
@@ -88,9 +87,6 @@ let rec parse_user_entry s sep =
   else
     Uentry s
 
-let arg_list = function Rawwit t -> Rawwit (ListArg t)
-let arg_opt = function Rawwit t -> Rawwit (OptArg t)
-
 let interp_entry_name interp symb =
   let rec eval = function
   | Ulist1 e -> Ulist1 (eval e)
@@ -178,9 +174,9 @@ let add_tactic_entry (kn, ml, tg) state =
   in
   let map = function
   | TacTerm s -> GramTerminal s
-  | TacNonTerm (loc, (s, _)) ->
+  | TacNonTerm (loc, (s, ido)) ->
     let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in
-    GramNonTerminal (Loc.tag ?loc (typ, e))
+    GramNonTerminal (Loc.tag ?loc @@ (Option.map (fun _ -> typ) ido, e))
   in
   let prods = List.map map tg.tacgram_prods in
   let rules = make_rule mkact prods in
@@ -206,7 +202,7 @@ let register_tactic_notation_entry name entry =
 
 let interp_prod_item = function
   | TacTerm s -> TacTerm s
-  | TacNonTerm (loc, ((nt, sep), id)) ->
+  | TacNonTerm (loc, ((nt, sep), ido)) ->
     let symbol = parse_user_entry nt sep in
     let interp s = function
     | None ->
@@ -224,7 +220,7 @@ let interp_prod_item = function
       end
     in
     let symbol = interp_entry_name interp symbol in
-    TacNonTerm (loc, (symbol, id))
+    TacNonTerm (loc, (symbol, ido))
 
 let make_fresh_key =
   let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
@@ -300,7 +296,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj =
 
 let cons_production_parameter = function
 | TacTerm _ -> None
-| TacNonTerm (_, (_, id)) -> Some id
+| TacNonTerm (_, (_, ido)) -> ido
 
 let add_glob_tactic_notation local ~level prods forml ids tac =
   let parule = {
@@ -320,7 +316,7 @@ let add_tactic_notation local n prods e =
   let ids = List.map_filter cons_production_parameter prods in
   let prods = List.map interp_prod_item prods in
   let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
-  add_glob_tactic_notation local n prods false ids tac
+  add_glob_tactic_notation local ~level:n prods false ids tac
 
 (**********************************************************************)
 (* ML Tactic entries                                                  *)
@@ -366,7 +362,7 @@ let add_ml_tactic_notation name ~level prods =
     let open Tacexpr in
     let get_id = function
     | TacTerm s -> None
-    | TacNonTerm (_, (_, id)) -> Some id
+    | TacNonTerm (_, (_, ido)) -> ido
     in
     let ids = List.map_filter get_id prods in
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in