diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 53c317c0..1b04b117 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -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 *) @@ -211,6 +211,7 @@ module Tactic : sig open Glob_term val open_constr : open_constr_expr Gram.entry + val open_constr_wTC : open_constr_expr Gram.entry val casted_open_constr : open_constr_expr Gram.entry val constr_with_bindings : constr_expr with_bindings Gram.entry val bindings : constr_expr bindings Gram.entry |