aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/cic.mli
diff options
context:
space:
mode:
Diffstat (limited to 'checker/cic.mli')
-rw-r--r--checker/cic.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/cic.mli b/checker/cic.mli
index 881d3ca79..bd75111a2 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -380,7 +380,7 @@ and module_body =
(** algebraic type, kept if it's relevant for extraction *)
mod_type_alg : module_expression option;
(** set of all constraints in the module *)
- mod_constraints : Univ.constraints;
+ mod_constraints : Univ.ContextSet.t;
(** quotiented set of equivalent constants and inductive names *)
mod_delta : delta_resolver;
mod_retroknowledge : action list }