grammar: export hypident

This is necessary to make ssr compile with both camlp4/5

5 files changed, 8 insertions, 1 deletions

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 3f232c3612..a7241399e0 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -55,6 +55,9 @@ let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType
 
 let wit_bindings = unsafe_of_type BindingsArgType
 
+let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type =
+  Genarg.make0 None "hyp_location_flag"
+
 let wit_red_expr = unsafe_of_type RedExprArgType
 
 let wit_clause_dft_concl  =
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 74c6bd310c..fdeddd66a1 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -64,6 +64,8 @@ val wit_bindings :
   glob_constr_and_expr bindings,
   constr bindings Evd.sigma) genarg_type
 
+val wit_hyp_location_flag : Locus.hyp_location_flag uniform_genarg_type
+
 val wit_red_expr :
   ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index b42b2c6dd3..69593f993c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -202,7 +202,7 @@ let merge_occurrences loc cl = function
 GEXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
   bindings red_expr int_or_var open_constr uconstr
-  simple_intropattern clause_dft_concl;
+  simple_intropattern clause_dft_concl hypident;
 
   int_or_var:
     [ [ n = integer  -> ArgArg n
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index cf6435fec4..6a9848c1ca 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -375,6 +375,7 @@ module Tactic =
       make_gen_entry utactic (rawwit wit_constr_with_bindings) "constr_with_bindings"
     let bindings =
       make_gen_entry utactic (rawwit wit_bindings) "bindings"
+    let hypident = Gram.entry_create "hypident"
     let constr_may_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval"
     let uconstr =
       make_gen_entry utactic (rawwit wit_uconstr) "uconstr"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index dbd2aadf9d..e23b65e12c 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -215,6 +215,7 @@ module Tactic :
     val open_constr : open_constr_expr Gram.entry
     val constr_with_bindings : constr_expr with_bindings Gram.entry
     val bindings : constr_expr bindings Gram.entry
+    val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry
     val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
     val uconstr : constr_expr Gram.entry
     val quantified_hypothesis : quantified_hypothesis Gram.entry