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/rewrite.mli | |
| parent | 679132dd7b193c5d19066696871ca13fafc35654 (diff) | |
Removing unused tactics in rewrite.
Diffstat (limited to 'tactics/rewrite.mli')
| -rw-r--r-- | tactics/rewrite.mli | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli index 63166c64a..e2d9a41d8 100644 --- a/tactics/rewrite.mli +++ b/tactics/rewrite.mli @@ -78,11 +78,3 @@ val setoid_symmetry_in : Id.t -> unit Proofview.tactic val setoid_reflexivity : unit Proofview.tactic val setoid_transitivity : constr option -> unit Proofview.tactic - -val implify : Id.t -> tactic - -val fold_match_tac : constr -> tactic - -val fold_matches_tac : constr -> tactic - -val myapply : Globnames.global_reference -> constr list -> tactic |