diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-01-14 09:03:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-01-14 09:03:44 +0100 |
| commit | b8d31eb7f359dd842c1b53b1b74725158fc01c1e (patch) | |
| tree | 496463f667544a45565ae549ddba4a2b77c6a1ee /tactics/g_rewrite.ml4 | |
| parent | 679132dd7b193c5d19066696871ca13fafc35654 (diff) | |
Removing unused tactics in rewrite.
Diffstat (limited to 'tactics/g_rewrite.ml4')
| -rw-r--r-- | tactics/g_rewrite.ml4 | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index 31defcafb..db98c4250 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -265,19 +265,3 @@ TACTIC EXTEND setoid_transitivity [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ] | [ "setoid_etransitivity" ] -> [ setoid_transitivity None ] END - -TACTIC EXTEND implify -[ "implify" hyp(n) ] -> [ Proofview.V82.tactic (implify n) ] -END - -TACTIC EXTEND fold_match -[ "fold_match" constr(c) ] -> [ Proofview.V82.tactic (fold_match_tac c) ] -END - -TACTIC EXTEND fold_matches -| [ "fold_matches" constr(c) ] -> [ Proofview.V82.tactic (fold_matches_tac c) ] -END - -TACTIC EXTEND myapply -| [ "myapply" global(id) constr_list(l) ] -> [ Proofview.V82.tactic (myapply id l) ] -END |