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 9fd7172a5..5139cf051 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -48,7 +48,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
type cooking_info = {
modlist : work_list;
- abstract : Context.named_context * Univ.universe_level_subst * Univ.UContext.t }
+ abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t }
(* The type has two caveats:
1) cook_constr is defined after