aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/univGen.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/univGen.mli')
-rw-r--r--engine/univGen.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/univGen.mli b/engine/univGen.mli
index 8169dbda4..439424934 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -39,7 +39,7 @@ val fresh_instance_from_context : AUContext.t ->
val fresh_instance_from : AUContext.t -> Instance.t option ->
Instance.t in_universe_context_set
-val fresh_sort_in_family : env -> Sorts.family ->
+val fresh_sort_in_family : Sorts.family ->
Sorts.t in_universe_context_set
val fresh_constant_instance : env -> Constant.t ->
pconstant in_universe_context_set