From 41e4725805588b3fffdfdc0cd5ee6859de1612b5 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 30 Mar 2015 11:26:58 +0200
Subject: grammar: export constr_eval

---
 parsing/g_ltac.ml4 | 2 +-
 parsing/pcoq.ml4   | 1 +
 parsing/pcoq.mli   | 1 +
 3 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 3cd7dbc9be..a4dba506d2 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -33,7 +33,7 @@ let genarg_of_ipattern pat = in_gen (rawwit Constrarg.wit_intro_pattern) pat
 
 GEXTEND Gram
   GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg
-          constr_may_eval;
+          constr_may_eval constr_eval;
 
   tactic_then_last:
     [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" ->
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 6a9848c1ca..54edbb2c88 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -377,6 +377,7 @@ module Tactic =
       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 constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval"
     let uconstr =
       make_gen_entry utactic (rawwit wit_uconstr) "uconstr"
     let quantified_hypothesis =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index e23b65e12c..2146ad964f 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -217,6 +217,7 @@ module Tactic :
     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 constr_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
     val int_or_var : int or_var Gram.entry
-- 
cgit v1.2.3