diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-22 12:11:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-04-22 12:20:27 +0200 |
| commit | 17b84de9ec0b14006dda0e1588f04a830ac5995f (patch) | |
| tree | 9722282adcefd3d97f0de76ec31f0405c826359b /tactics/leminv.mli | |
| parent | f76c0b3b89ce433de5cad7d35c437ce26f1e7477 (diff) | |
Removing the compatibility layer from Leminv. Also removed an undocumented
variant of the Derive Inversion command which took the current goal as the
targeted inductive. It was unused in the contribs and it seemed rather
bad from the STM point of view, as it generated a lemma inside a proof.
Diffstat (limited to 'tactics/leminv.mli')
| -rw-r--r-- | tactics/leminv.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 36aa5e67f..76223abed 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -18,9 +18,6 @@ val lemInvIn_gen : quantified_hypothesis -> constr -> Id.t list -> unit Proofvie val lemInv_clause : quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic -val inversion_lemma_from_goal : - int -> Id.t -> Id.t located -> sorts -> bool -> - (Id.t -> unit Proofview.tactic) -> unit val add_inversion_lemma_exn : Id.t -> constr_expr -> glob_sort -> bool -> (Id.t -> unit Proofview.tactic) -> unit |