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 23ef84c55d..8855a6bea6 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -100,7 +100,7 @@ val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t ->
universes are preserved. *)
val restrict : t -> Univ.LSet.t -> t
-type rigid =
+type rigid =
| UnivRigid
| UnivFlexible of bool (** Is substitution by an algebraic ok? *)