aboutsummaryrefslogtreecommitdiff
path: root/engine/uState.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/uState.mli')
-rw-r--r--engine/uState.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/uState.mli b/engine/uState.mli
index 9dc96622ea..c5c454020c 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -84,11 +84,11 @@ val univ_rigid : rigid
val univ_flexible : rigid
val univ_flexible_alg : rigid
-val merge : bool -> rigid -> t -> Univ.universe_context_set -> t
+val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.universe_context_set -> t
val merge_subst : t -> Universes.universe_opt_subst -> t
val emit_side_effects : Safe_typing.private_constants -> t -> t
-val new_univ_variable : rigid -> string option -> t -> t * Univ.Level.t
+val new_univ_variable : ?loc:Loc.t -> rigid -> string option -> t -> t * Univ.Level.t
val add_global_univ : t -> Univ.Level.t -> t
val make_flexible_variable : t -> bool -> Univ.Level.t -> t