aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/universes.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/universes.mli')
-rw-r--r--engine/universes.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/universes.mli b/engine/universes.mli
index 29673de1e..306ba0db0 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -86,7 +86,7 @@ val fresh_instance_from : AUContext.t -> Instance.t option ->
Instance.t in_universe_context_set
[@@ocaml.deprecated "Use [UnivGen.fresh_instance_from]"]
-val fresh_sort_in_family : env -> Sorts.family ->
+val fresh_sort_in_family : Sorts.family ->
Sorts.t in_universe_context_set
[@@ocaml.deprecated "Use [UnivGen.fresh_sort_in_family]"]