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 7e13f8f28..0e2b0c80e 100644
--- a/vernac/assumptions.mli
+++ b/vernac/assumptions.mli
@@ -30,4 +30,4 @@ val traverse :
{!traverse} also applies. *)
val assumptions :
?add_opaque:bool -> ?add_transparent:bool -> transparent_state ->
- global_reference -> constr -> types ContextObjectMap.t
+ GlobRef.t -> constr -> types ContextObjectMap.t