aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/assumptions.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/assumptions.mli')
-rw-r--r--vernac/assumptions.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli
index 77eb968d4..afe932ead 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Names
-open Term
+open Constr
open Globnames
open Printer
@@ -28,4 +28,4 @@ val traverse :
{!traverse} also applies. *)
val assumptions :
?add_opaque:bool -> ?add_transparent:bool -> transparent_state ->
- global_reference -> constr -> Term.types ContextObjectMap.t
+ global_reference -> constr -> types ContextObjectMap.t