aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/uState.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/uState.ml')
-rw-r--r--engine/uState.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/uState.ml b/engine/uState.ml
index 13a9bb373..77837fefc 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -33,10 +33,10 @@ type uinfo = {
(* 2nd part used to check consistency on the fly. *)
type t =
{ uctx_names : Univ.Level.t UNameMap.t * uinfo Univ.LMap.t;
- uctx_local : Univ.universe_context_set; (** The local context of variables *)
+ uctx_local : Univ.ContextSet.t; (** The local context of variables *)
uctx_univ_variables : Universes.universe_opt_subst;
(** The local universes that are unification variables *)
- uctx_univ_algebraic : Univ.universe_set;
+ uctx_univ_algebraic : Univ.LSet.t;
(** The subset of unification variables that can be instantiated with
algebraic universes as they appear in inferred types only. *)
uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)