From 5fb2050e424062540ffbf22de0838fafe4de0a41 Mon Sep 17 00:00:00 2001
From: Julien Forest
Date: Mon, 14 Apr 2014 23:22:14 +0200
Subject: Closing bug #3260 adding a new grammar entry for clauses

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

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 93afb3d5ae..6b989b6baf 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -216,7 +216,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
-  simple_intropattern;
+  simple_intropattern clause_dft_concl;
 
   int_or_var:
     [ [ n = integer  -> ArgArg n
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 6fac3da965..473e095dc9 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -388,6 +388,9 @@ module Tactic =
     let red_expr = make_gen_entry utactic (rawwit wit_red_expr) "red_expr"
     let simple_intropattern =
       make_gen_entry utactic (rawwit wit_intro_pattern) "simple_intropattern"
+    let clause_dft_concl = 
+      make_gen_entry utactic (rawwit wit_clause_dft_concl) "clause"
+
 
     (* Main entries for ltac *)
     let tactic_arg = Gram.entry_create "tactic:tactic_arg"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 3fb647a96c..cf98e5a542 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -218,6 +218,7 @@ module Tactic :
     val red_expr : raw_red_expr Gram.entry
     val simple_tactic : raw_atomic_tactic_expr Gram.entry
     val simple_intropattern : intro_pattern_expr located Gram.entry
+    val clause_dft_concl : Names.Id.t Loc.located Tacexpr.or_metaid Locus.clause_expr Gram.entry
     val tactic_arg : raw_tactic_arg Gram.entry
     val tactic_expr : raw_tactic_expr Gram.entry
     val binder_tactic : raw_tactic_expr Gram.entry
-- 
cgit v1.2.3