Indexing existentially quantified entries returned by interp_entry_name.

11 files changed, 25 insertions, 23 deletions

diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 7c20ff18e9..51949e8aad 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -51,8 +51,8 @@ let make_rawwit loc arg = <:expr< Genarg.rawwit $make_wit loc arg$ >>
 let make_globwit loc arg = <:expr< Genarg.glbwit $make_wit loc arg$ >>
 let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
 
-let has_extraarg =
-  List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false)
+let has_extraarg l =
+  List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false) l
 
 let rec is_possibly_empty : type s a. (s, a) entry_key -> bool = function
 | Aopt _ -> true
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 4709a79989..2c9a73a371 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -100,8 +100,8 @@ let make_prod_item = function
       <:expr< Egramml.GramNonTerminal $default_loc$ $mlexpr_of_argtype loc nt$
       $mlexpr_of_prod_entry_key g$ $mlexpr_of_option mlexpr_of_ident sopt$ >>
 
-let mlexpr_of_clause =
-  mlexpr_of_list (fun (a,_,b) -> mlexpr_of_list make_prod_item a)
+let mlexpr_of_clause cl =
+  mlexpr_of_list (fun (a,_,b) -> mlexpr_of_list make_prod_item a) cl
 
 let rec make_tags loc = function
   | [] -> <:expr< [] >>
@@ -120,7 +120,7 @@ let make_one_printing_rule (pt,_,e) =
   <:expr< { Pptactic.pptac_args = $make_tags loc pt$;
             pptac_prods = ($level$, $prods$) } >>
 
-let make_printing_rule = mlexpr_of_list make_one_printing_rule
+let make_printing_rule r = mlexpr_of_list make_one_printing_rule r
 
 let make_empty_check = function
 | GramNonTerminal(_, t, e, _)->
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index d99af6a33d..f0fde2bf84 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -22,7 +22,7 @@ open Compat
 type rule = {
   r_head : string option;
   (** The first terminal grammar token *)
-  r_patt : grammar_prod_item list;
+  r_patt : Vernacexpr.vernac_expr grammar_prod_item list;
   (** The remaining tokens of the parsing rule *)
   r_class : MLast.expr option;
   (** An optional classifier for the STM *)
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 7bfcf65e3e..14fe15e89e 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -246,13 +246,13 @@ let get_tactic_entry n =
 
 type tactic_grammar = {
   tacgram_level : int;
-  tacgram_prods : grammar_prod_item list;
+  tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
 }
 
 type all_grammar_command =
   | Notation of Notation.level * notation_grammar
   | TacticGrammar of KerName.t * tactic_grammar
-  | MLTacticGrammar of ml_tactic_name * grammar_prod_item list list
+  | MLTacticGrammar of ml_tactic_name * Tacexpr.raw_tactic_expr grammar_prod_item list list
 
 (** ML Tactic grammar extensions *)
 
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 2b0f7da8c2..cdd5fbd0f9 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -38,7 +38,7 @@ type notation_grammar = {
 
 type tactic_grammar = {
   tacgram_level : int;
-  tacgram_prods : grammar_prod_item list;
+  tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list;
 }
 
 (** {5 Adding notations} *)
@@ -50,7 +50,7 @@ val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit
 (** Add a tactic notation rule to the parsing system. This produces a TacAlias
     tactic with the provided kernel name. *)
 
-val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> grammar_prod_item list list -> unit
+val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> Tacexpr.raw_tactic_expr grammar_prod_item list list -> unit
 (** Add a ML tactic notation rule to the parsing system. This produces a
     TacML tactic with the provided string as name. *)
 
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 8f07087085..77d60ff7d5 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -28,10 +28,10 @@ let make_generic_action
 
 (** Grammar extensions declared at ML level *)
 
-type grammar_prod_item =
+type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal :
-      Loc.t * argument_type * ('s, 'a) entry_key * Id.t option -> grammar_prod_item
+      Loc.t * argument_type * ('s, 'a) entry_key * Id.t option -> 's grammar_prod_item
 
 let make_prod_item = function
   | GramTerminal s -> (gram_token_of_string s, None)
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 60ec6a05a8..182a72086f 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -6,24 +6,26 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Vernacexpr
+
 (** Mapping of grammar productions to camlp4 actions. *)
 
 (** This is the part specific to vernac extensions.
     For the Coq-level Notation and Tactic Notation, see Egramcoq. *)
 
-type grammar_prod_item =
+type 's grammar_prod_item =
   | GramTerminal of string
   | GramNonTerminal : Loc.t * Genarg.argument_type *
-      ('s, 'a) Pcoq.entry_key * Names.Id.t option -> grammar_prod_item
+      ('s, 'a) Pcoq.entry_key * Names.Id.t option -> 's grammar_prod_item
 
 val extend_vernac_command_grammar :
-  Vernacexpr.extend_name -> Vernacexpr.vernac_expr Pcoq.Gram.entry option ->
-    grammar_prod_item list -> unit
+  Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option ->
+    vernac_expr grammar_prod_item list -> unit
 
-val get_extend_vernac_rule : Vernacexpr.extend_name -> grammar_prod_item list
+val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list
 
 (** Utility function reused in Egramcoq : *)
 
 val make_rule :
   (Loc.t -> (Names.Id.t * Genarg.raw_generic_argument) list -> 'b) ->
-  grammar_prod_item list -> Pcoq.Gram.symbol list * Pcoq.Gram.action
+  's grammar_prod_item list -> Pcoq.Gram.symbol list * Pcoq.Gram.action
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 1dea3497e4..2227f7e9ce 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -80,7 +80,7 @@ type ('self, 'a) entry_key = ('self, 'a) Extend.symbol =
 | Aentry : 'a Entry.t -> ('self, 'a) entry_key
 | Aentryl : 'a Entry.t * int -> ('self, 'a) entry_key
 
-type entry_name = EntryName : entry_type * ('self, 'a) entry_key -> entry_name
+type 's entry_name = EntryName : entry_type * ('s, 'a) entry_key -> 's entry_name
 
 module type Gramtypes =
 sig
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 74b7bcc93f..8a1bc884a1 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -285,12 +285,12 @@ val name_of_entry : 'a Gram.entry -> 'a Entry.t
 val symbol_of_prod_entry_key :
   ('self, 'a) entry_key -> Gram.symbol
 
-type entry_name = EntryName : entry_type * ('self, 'a) entry_key -> entry_name
+type 's entry_name = EntryName : entry_type * ('s, 'a) entry_key -> 's entry_name
 
 (** Interpret entry names of the form "ne_constr_list" as entry keys   *)
 
 val interp_entry_name : bool (** true to fail on unknown entry *) ->
-  int option -> string -> string -> entry_name
+  int option -> string -> string -> 's entry_name
 
 (** Recover the list of all known tactic notation entries. *)
 val list_entry_names : unit -> (string * entry_type) list
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 780a8f111c..ca263e6cbb 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -160,7 +160,7 @@ type atomic_entry = string * Genarg.glob_generic_argument list option
 type ml_tactic_grammar_obj = {
   mltacobj_name : Tacexpr.ml_tactic_name;
   (** ML-side unique name *)
-  mltacobj_prod : grammar_prod_item list list;
+  mltacobj_prod : Tacexpr.raw_tactic_expr grammar_prod_item list list;
   (** Grammar rules generating the ML tactic. *)
 }
 
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index f22839f489..f7049999e1 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -24,7 +24,7 @@ val add_tactic_notation :
 type atomic_entry = string * Genarg.glob_generic_argument list option
 
 val add_ml_tactic_notation : ml_tactic_name ->
-  Egramml.grammar_prod_item list list -> atomic_entry list -> unit
+  Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> atomic_entry list -> unit
 
 (** Adding a (constr) notation in the environment*)