diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-05 12:14:30 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-05 16:52:13 +0200 |
| commit | 076ac1757383cd9e3f505c3f958c1757087011ac (patch) | |
| tree | e962c04eb294689b901a87cfe5dab530d9c4fbfb | |
| parent | b19a845e7bbda10120a8a1f4b5cf92a057b5d10f (diff) | |
Properly declare uconstr as an argument for TACTIC EXTEND.
| -rw-r--r-- | parsing/g_tactic.ml4 | 5 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 2 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
3 files changed, 7 insertions, 1 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 77461213b..4c328a3bf 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 + bindings red_expr int_or_var open_constr uconstr simple_intropattern clause_dft_concl; int_or_var: @@ -233,6 +233,9 @@ GEXTEND Gram open_constr: [ [ c = constr -> ((),c) ] ] ; + uconstr: + [ [ 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 c2d28d36c..64a705c2c 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -382,6 +382,8 @@ module Tactic = let bindings = make_gen_entry utactic (rawwit wit_bindings) "bindings" let constr_may_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval" + let uconstr = + make_gen_entry utactic (rawwit wit_uconstr) "uconstr" let quantified_hypothesis = make_gen_entry utactic (rawwit wit_quant_hyp) "quantified_hypothesis" let int_or_var = make_gen_entry utactic (rawwit wit_int_or_var) "int_or_var" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 7d138efa3..61ca13787 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -213,6 +213,7 @@ module Tactic : 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 + val uconstr : constr_expr Gram.entry val quantified_hypothesis : quantified_hypothesis Gram.entry val int_or_var : int or_var Gram.entry val red_expr : raw_red_expr Gram.entry |