From 420f78b2caeaaddc6fe484565b2d0e49c66888e5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 27 Jul 2014 10:02:38 +0200
Subject: Imported Upstream version 8.4pl4dfsg

---
 parsing/pcoq.ml4 | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'parsing/pcoq.ml4')

diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 7f11af93..7949a77d 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -380,9 +380,11 @@ module Tactic =
     (* Entries that can be refered via the string -> Gram.entry table *)
     (* Typically for tactic user extensions *)
     let open_constr =
-      make_gen_entry utactic (rawwit_open_constr_gen false) "open_constr"
+      make_gen_entry utactic (rawwit_open_constr_gen (false,false)) "open_constr"
     let casted_open_constr =
-      make_gen_entry utactic (rawwit_open_constr_gen true) "casted_open_constr"
+      make_gen_entry utactic (rawwit_open_constr_gen (true,false)) "casted_open_constr"
+    let open_constr_wTC =
+      make_gen_entry utactic (rawwit_open_constr_gen (false,true)) "open_constr_wTC"
     let constr_with_bindings =
       make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings"
     let bindings =
-- 
cgit v1.2.3