Merge branch 'trunk' into located_switch

5 files changed, 31 insertions, 20 deletions

diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
index 10ead2c29..c736e1a74 100644
--- a/grammar/argextend.mlp
+++ b/grammar/argextend.mlp
@@ -39,7 +39,8 @@ let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
 let make_act loc act pil =
   let rec make = function
     | [] -> <:expr< (fun loc -> $act$) >>
-    | ExtNonTerminal (_, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >>
+    | ExtNonTerminal (_, None) :: tl -> <:expr< (fun $lid:"_"$ -> $make tl$) >>
+    | ExtNonTerminal (_, Some p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >>
     | ExtTerminal _ :: tl ->
 	<:expr< (fun _ -> $make tl$) >> in
   make (List.rev pil)
@@ -62,7 +63,7 @@ let is_ident x = function
 | _ -> false
 
 let make_extend loc s cl wit = match cl with
-| [[ExtNonTerminal (Uentry e, id)], act] when is_ident id act ->
+| [[ExtNonTerminal (Uentry e, Some id)], act] when is_ident id act ->
   (** Special handling of identity arguments by not redeclaring an entry *)
   <:str_item<
     value $lid:s$ =
@@ -245,10 +246,13 @@ EXTEND
   genarg:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
-        ExtNonTerminal (e, s)
+        ExtNonTerminal (e, Some s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
-        ExtNonTerminal (e, s)
+        ExtNonTerminal (e, Some s)
+      | e = LIDENT ->
+        let e = parse_user_entry e "" in
+        ExtNonTerminal (e, None)
       | s = STRING -> ExtTerminal s
     ] ]
   ;
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 5b3eb3202..0b3def058 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -23,7 +23,7 @@ type user_symbol =
 
 type extend_token =
 | ExtTerminal of string
-| ExtNonTerminal of user_symbol * string
+| ExtNonTerminal of user_symbol * string option
 
 val mlexpr_of_list :  ('a -> MLast.expr) -> 'a list -> MLast.expr
 
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 8b930cf36..87262e1c8 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -25,7 +25,7 @@ type user_symbol =
 
 type extend_token =
 | ExtTerminal of string
-| ExtNonTerminal of user_symbol * string
+| ExtNonTerminal of user_symbol * string option
 
 let mlexpr_of_list f l =
   List.fold_right
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index aa463ada5..8e3dccf47 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -29,19 +29,19 @@ let mlexpr_of_ident id =
 
 let rec make_patt = function
   | [] -> <:patt< [] >>
-  | ExtNonTerminal (_, p) :: l ->
+  | ExtNonTerminal (_, Some p) :: l ->
       <:patt< [ $lid:p$ :: $make_patt l$ ] >>
   | _::l -> make_patt l
 
 let rec make_let raw e = function
   | [] -> <:expr< fun $lid:"ist"$ -> $e$ >>
-  | ExtNonTerminal (g, p) :: l ->
+  | ExtNonTerminal (g, Some p) :: l ->
       let t = type_of_user_symbol g in
       let loc = MLast.loc_of_expr e in
       let e = make_let raw e l in
       let v =
         if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >>
-               else <:expr< Tacinterp.Value.cast $make_topwit    loc t$ $lid:p$ >> in
+               else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in
       <:expr< let $lid:p$ = $v$ in $e$ >>
   | _::l -> make_let raw e l
 
@@ -73,7 +73,7 @@ let rec mlexpr_of_symbol = function
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >>
   | ExtNonTerminal (g, id) ->
-    <:expr< Tacentries.TacNonTerm (Loc.tag ( $mlexpr_of_symbol g$ , $mlexpr_of_ident id$ ) ) >>
+    <:expr< Tacentries.TacNonTerm (Loc.tag ( $mlexpr_of_symbol g$ , $mlexpr_of_option mlexpr_of_ident id$ ) ) >>
 
 let mlexpr_of_clause cl =
   mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl
@@ -85,7 +85,7 @@ let is_constr_gram = function
 | _ -> false
 
 let make_var = function
-  | ExtNonTerminal (_, p) -> Some p
+  | ExtNonTerminal (_, p) -> p
   | _ -> assert false
 
 let declare_tactic loc tacname ~level classification clause = match clause with
@@ -127,7 +127,7 @@ let declare_tactic loc tacname ~level classification clause = match clause with
   let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in
   let gl = mlexpr_of_clause clause in
   let level = mlexpr_of_int level in
-  let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $level$ $gl$ >> in
+  let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ ~{ level = $level$ } $gl$ >> in
   declare_str_items loc
     [ <:str_item< do {
         Tacenv.register_ml_tactic $se$ (Array.of_list $make_fun_clauses loc tacname clause$);
@@ -156,10 +156,13 @@ EXTEND
   tacargs:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
-        ExtNonTerminal (e, s)
+        ExtNonTerminal (e, Some s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
-        ExtNonTerminal (e, s)
+        ExtNonTerminal (e, Some s)
+      | e = LIDENT ->
+        let e = parse_user_entry e "" in
+        ExtNonTerminal (e, None)
       | s = STRING ->
 	let () = if s = "" then failwith "Empty terminal." in
         ExtTerminal s
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index 39155a014..4f9a7c75c 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -27,7 +27,7 @@ type rule = {
 
 let rec make_let e = function
   | [] -> e
-  | ExtNonTerminal (g, p) :: l ->
+  | ExtNonTerminal (g, Some p) :: l ->
       let t = type_of_user_symbol g in
       let loc = MLast.loc_of_expr e in
       let e = make_let e l in
@@ -42,7 +42,7 @@ let make_clause { r_patt = pt; r_branch = e; } =
 (* To avoid warnings *)
 let mk_ignore c pt =
   let fold accu = function
-  | ExtNonTerminal (_, p) -> p :: accu
+  | ExtNonTerminal (_, Some p) -> p :: accu
   | _ -> accu
   in
   let names = List.fold_left fold [] pt in
@@ -101,10 +101,11 @@ let make_fun_classifiers loc s c l =
 
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
-  | ExtNonTerminal (g, id) ->
+  | ExtNonTerminal (g, ido) ->
     let nt = type_of_user_symbol g in
     let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in
-      <:expr< Egramml.GramNonTerminal ( Loc.tag ( $make_rawwit loc nt$ ,
+    let typ = match ido with None -> None | Some _ -> Some nt in
+      <:expr< Egramml.GramNonTerminal ( Loc.tag ( $mlexpr_of_option (make_rawwit loc) typ$ ,
       $mlexpr_of_prod_entry_key base g$ ) ) >>
 
 let mlexpr_of_clause cl =
@@ -178,10 +179,13 @@ EXTEND
   args:
     [ [ e = LIDENT; "("; s = LIDENT; ")" ->
         let e = parse_user_entry e "" in
-        ExtNonTerminal (e, s)
+        ExtNonTerminal (e, Some s)
       | e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
         let e = parse_user_entry e sep in
-        ExtNonTerminal (e, s)
+        ExtNonTerminal (e, Some s)
+      | e = LIDENT ->
+        let e = parse_user_entry e "" in
+        ExtNonTerminal (e, None)
       | s = STRING ->
         ExtTerminal s
     ] ]