diff options
| author | Pierre-Marie Pédrot | 2013-11-25 22:30:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-11-30 17:00:34 +0100 |
| commit | a01a60b366307da3eca63c9937984db6f273dc41 (patch) | |
| tree | c8a5f42e5db1fd763367390a49d0611a68e33bf5 /parsing | |
| parent | b86e7c1247fa4b34b75cf20ef24a8e0b6ba6eff1 (diff) | |
Getting rid of casted_open_constr. It was only used by the
refine tactic, which now uses plain glob_constr's. Now there
is no real need to depend on goal when interpreting genargs.
Possible minor incompatibilities:
1. The interpretation of glob_constr to constr is now done by
Goal.constr_of_raw, which may be slightly dumbier than the dedicated
Tacinterp.interp_open_constr which tries harder. Stdlib and test-suite
do go through, though.
2. I had to change the parsing level of wit_glob in Extraargs
from lconstr to constr. It may break ML notations using glob, but
as they are only used inside Coq code and all well-parenthezised,
it should be OK.
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 |