diff options
| author | Hugo Herbelin | 2015-12-20 01:04:15 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-18 13:07:22 +0200 |
| commit | 2cb554aa772c5c6d179c6a4611b70d459073a316 (patch) | |
| tree | 4493ad52bb7adf03128de2bba63d46f26a893a77 /parsing | |
| parent | 403af31e3d0bc571acf0a66907277ad839c94df4 (diff) | |
Exporting a generic argument induction_arg. As a consequence,
simplifying and generalizing the grammar entries for injection,
discriminate and simplify_eq.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 14 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 2 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
3 files changed, 10 insertions, 7 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index a8a88d33f4..d0bca9ee3f 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -141,7 +141,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) = (id,CProdN(loc,bl,ty)) (* Functions overloaded by quotifier *) -let induction_arg_of_constr (c,lbind as clbind) = match lbind with +let destruction_arg_of_constr (c,lbind as clbind) = match lbind with | NoBindings -> begin try ElimOnIdent (Constrexpr_ops.constr_loc c,snd(Constrexpr_ops.coerce_to_id c)) @@ -216,7 +216,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 uconstr - simple_intropattern clause_dft_concl hypident; + simple_intropattern clause_dft_concl hypident destruction_arg; int_or_var: [ [ n = integer -> ArgArg n @@ -236,11 +236,11 @@ GEXTEND Gram uconstr: [ [ c = constr -> c ] ] ; - induction_arg: + destruction_arg: [ [ n = natural -> (None,ElimOnAnonHyp n) | test_lpar_id_rpar; c = constr_with_bindings -> - (Some false,induction_arg_of_constr c) - | c = constr_with_bindings_arg -> on_snd induction_arg_of_constr c + (Some false,destruction_arg_of_constr c) + | c = constr_with_bindings_arg -> on_snd destruction_arg_of_constr c ] ] ; constr_with_bindings_arg: @@ -499,8 +499,8 @@ GEXTEND Gram [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ] ; induction_clause: - [ [ c = induction_arg; pat = as_or_and_ipat; eq = eqn_ipat; cl = opt_clause - -> (c,(eq,pat),cl) ] ] + [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat; + cl = opt_clause -> (c,(eq,pat),cl) ] ] ; induction_clause_list: [ [ ic = LIST1 induction_clause SEP ","; el = OPT eliminator; diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index efb89cd6e1..7d1c63ee06 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -345,6 +345,7 @@ module Tactic = make_gen_entry utactic "uconstr" let quantified_hypothesis = make_gen_entry utactic "quantified_hypothesis" + let destruction_arg = make_gen_entry utactic "destruction_arg" let int_or_var = make_gen_entry utactic "int_or_var" let red_expr = make_gen_entry utactic "red_expr" let simple_intropattern = @@ -520,4 +521,5 @@ let () = Grammar.register0 wit_tactic (Tactic.tactic); Grammar.register0 wit_ltac (Tactic.tactic); Grammar.register0 wit_clause_dft_concl (Tactic.clause_dft_concl); + Grammar.register0 wit_destruction_arg (Tactic.destruction_arg); () diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 319ca256e1..008374e091 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -188,6 +188,7 @@ module Tactic : val constr_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 destruction_arg : constr_expr with_bindings destruction_arg Gram.entry val int_or_var : int or_var Gram.entry val red_expr : raw_red_expr Gram.entry val simple_tactic : raw_tactic_expr Gram.entry |