aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/assumptions.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/assumptions.mli')
-rw-r--r--toplevel/assumptions.mli3
1 files changed, 1 insertions, 2 deletions
diff --git a/toplevel/assumptions.mli b/toplevel/assumptions.mli
index 666218fe7..072675783 100644
--- a/toplevel/assumptions.mli
+++ b/toplevel/assumptions.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Util
open Names
open Term
open Globnames
@@ -22,7 +21,7 @@ open Printer
val traverse :
Label.t -> constr ->
(Refset_env.t * Refset_env.t Refmap_env.t *
- (label * Context.rel_context * types) list Refmap_env.t)
+ (label * Context.Rel.t * types) list Refmap_env.t)
(** Collects all the assumptions (optionally including opaque definitions)
on which a term relies (together with their type). The above warning of