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 2337a7901..f42e5a8b0 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -11,7 +11,7 @@
open Names
open EConstr
open Constrexpr
-open Misctypes
+open Tactypes
val lemInv_clause :
quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic