aboutsummaryrefslogtreecommitdiffhomepage
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 8745ad397..f221b1fd9 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -14,6 +14,6 @@ open Misctypes
val lemInv_clause :
quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
-val add_inversion_lemma_exn :
+val add_inversion_lemma_exn : poly:bool ->
Id.t -> constr_expr -> Sorts.family -> bool -> (Id.t -> unit Proofview.tactic) ->
unit