aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/opaqueproof.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/opaqueproof.mli')
-rw-r--r--kernel/opaqueproof.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 3897d5e51..be1f4b13f 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -49,7 +49,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
type cooking_info = {
modlist : work_list;
- abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t }
+ abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t }
(* The type has two caveats:
1) cook_constr is defined after