diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 5 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 4 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
3 files changed, 2 insertions, 8 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index eb483c50cf..93afb3d5ae 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -215,7 +215,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 casted_open_constr + bindings red_expr int_or_var open_constr simple_intropattern; int_or_var: @@ -236,9 +236,6 @@ GEXTEND Gram open_constr: [ [ c = constr -> ((),c) ] ] ; - casted_open_constr: - [ [ c = constr -> ((),c) ] ] - ; induction_arg: [ [ n = natural -> ElimOnAnonHyp n | c = constr_with_bindings -> induction_arg_of_constr c diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 79228e9462..d25efa72a8 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -377,9 +377,7 @@ 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 (wit_open_constr_gen false)) "open_constr" - let casted_open_constr = - make_gen_entry utactic (rawwit (wit_open_constr_gen true)) "casted_open_constr" + make_gen_entry utactic (rawwit wit_open_constr) "open_constr" let constr_with_bindings = make_gen_entry utactic (rawwit wit_constr_with_bindings) "constr_with_bindings" let bindings = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index bbb71a1703..56282f2f67 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -213,7 +213,6 @@ module Tactic : sig open Glob_term val open_constr : 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 val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry |