diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 103 |
1 files changed, 6 insertions, 97 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 66716acd..ee01f839 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: extratactics.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: extratactics.ml4 11800 2009-01-18 18:34:15Z msozeau $ *) open Pp open Pcoq @@ -18,6 +18,7 @@ open Mod_subst open Names open Tacexpr open Rawterm +open Tactics (* Equality *) open Equality @@ -133,10 +134,10 @@ let h_injHyp id = h_injection_main (Term.mkVar id,NoBindings) TACTIC EXTEND conditional_rewrite | [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c) ] - -> [ conditional_rewrite b (snd tac) c ] + -> [ conditional_rewrite b (snd tac) (inj_open (fst c), snd c) ] | [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c) "in" hyp(h) ] - -> [ conditional_rewrite_in b h (snd tac) c ] + -> [ conditional_rewrite_in b h (snd tac) (inj_open (fst c), snd c) ] END TACTIC EXTEND dependent_rewrite @@ -216,87 +217,6 @@ END let refine_tac = h_refine -(* Setoid_replace *) - -open Setoid_replace - -(* TACTIC EXTEND setoid_replace *) -(* [ "setoid_replace" constr(c1) "with" constr(c2) by_arg_tac(tac)] -> *) -(* [ setoid_replace (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ] *) -(* | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) by_arg_tac(tac)] -> *) -(* [ setoid_replace (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ] *) -(* | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> *) -(* [ setoid_replace (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ] *) -(* | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> *) -(* [ setoid_replace (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ] *) -(* | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) by_arg_tac(tac) ] -> *) -(* [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ] *) -(* | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) by_arg_tac(tac)] -> *) -(* [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ] *) -(* | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> *) -(* [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ] *) -(* | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> *) -(* [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ] *) -(* END *) - -(* TACTIC EXTEND setoid_rewrite *) -(* [ "setoid_rewrite" orient(b) constr(c) ] *) -(* -> [ general_s_rewrite b c ~new_goals:[] ] *) -(* | [ "setoid_rewrite" orient(b) constr(c) "generate" "side" "conditions" constr_list(l) ] *) -(* -> [ general_s_rewrite b c ~new_goals:l ] *) -(* | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) ] -> *) -(* [ general_s_rewrite_in h b c ~new_goals:[] ] *) -(* | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] -> *) -(* [ general_s_rewrite_in h b c ~new_goals:l ] *) -(* END *) - -(* VERNAC COMMAND EXTEND AddSetoid1 *) -(* [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> *) -(* [ add_setoid n a aeq t ] *) -(* | [ "Add" "Morphism" constr(m) ":" ident(n) ] -> *) -(* [ new_named_morphism n m None ] *) -(* | [ "Add" "Morphism" constr(m) "with" "signature" morphism_signature(s) "as" ident(n) ] -> *) -(* [ new_named_morphism n m (Some s)] *) -(* END *) - -(* VERNAC COMMAND EXTEND AddRelation1 *) -(* [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "as" ident(n) ] -> *) -(* [ add_relation n a aeq (Some t) (Some t') None ] *) -(* | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "as" ident(n) ] -> *) -(* [ add_relation n a aeq (Some t) None None ] *) -(* | [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> *) -(* [ add_relation n a aeq None None None ] *) -(* END *) - -(* VERNAC COMMAND EXTEND AddRelation2 *) -(* [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "as" ident(n) ] -> *) -(* [ add_relation n a aeq None (Some t') None ] *) -(* | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'') "as" ident(n) ] -> *) -(* [ add_relation n a aeq None (Some t') (Some t'') ] *) -(* END *) - -(* VERNAC COMMAND EXTEND AddRelation3 *) -(* [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "transitivity" "proved" "by" constr(t') "as" ident(n) ] -> *) -(* [ add_relation n a aeq (Some t) None (Some t') ] *) -(* | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'') "as" ident(n) ] -> *) -(* [ add_relation n a aeq (Some t) (Some t') (Some t'') ] *) -(* | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(t) "as" ident(n) ] -> *) -(* [ add_relation n a aeq None None (Some t) ] *) -(* END *) - -(* TACTIC EXTEND setoid_symmetry *) -(* [ "setoid_symmetry" ] -> [ setoid_symmetry ] *) -(* | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ] *) -(* END *) - -(* TACTIC EXTEND setoid_reflexivity *) -(* [ "setoid_reflexivity" ] -> [ setoid_reflexivity ] *) -(* END *) - -(* TACTIC EXTEND setoid_transitivity *) -(* [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ] *) -(* END *) - (* Inversion lemmas (Leminv) *) open Inv @@ -485,17 +405,6 @@ END -TACTIC EXTEND apply_in -| ["apply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id) ] -> - [ apply_in false id cl ] -END - - -TACTIC EXTEND eapply_in -| ["eapply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id) ] -> - [ apply_in true id cl ] -END - (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as defined by Conor McBride *) TACTIC EXTEND generalize_eqs @@ -505,8 +414,8 @@ TACTIC EXTEND generalize_eqs_vars | ["generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize id ~generalize_vars:true ] END -TACTIC EXTEND conv -| ["conv" constr(x) constr(y) ] -> [ conv x y ] +TACTIC EXTEND dependent_pattern +| ["dependent_pattern" constr(c) ] -> [ dependent_pattern c ] END TACTIC EXTEND resolve_classes |