aboutsummaryrefslogtreecommitdiff
path: root/engine/uState.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/uState.mli')
-rw-r--r--engine/uState.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/uState.mli b/engine/uState.mli
index a59e61b894..f833508ebf 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -103,7 +103,7 @@ val univ_rigid : rigid
val univ_flexible : rigid
val univ_flexible_alg : rigid
-val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t
+val merge : ?loc:Loc.t -> sideff:bool -> extend:bool -> rigid -> t -> Univ.ContextSet.t -> t
val merge_subst : t -> UnivSubst.universe_opt_subst -> t
val emit_side_effects : Safe_typing.private_constants -> t -> t