aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/assumptions.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/assumptions.mli')
-rw-r--r--vernac/assumptions.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli
index 0e2b0c80e..751e79d89 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -23,7 +23,7 @@ open Printer
val traverse :
Label.t -> constr ->
(Refset_env.t * Refset_env.t Refmap_env.t *
- (Label.t * Context.Rel.t * types) list Refmap_env.t)
+ (Label.t * Constr.rel_context * 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