summaryrefslogtreecommitdiff
path: root/tactics/leminv.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/leminv.mli')
-rw-r--r--tactics/leminv.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 3e12f770..b4b5737b 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -8,7 +8,7 @@ open Topconstr
val lemInv_gen : quantified_hypothesis -> constr -> tactic
val lemInvIn_gen : quantified_hypothesis -> constr -> identifier list -> tactic
-val lemInv_clause :
+val lemInv_clause :
quantified_hypothesis -> constr -> identifier list -> tactic
val inversion_lemma_from_goal :