summaryrefslogtreecommitdiff
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 b6ae80b4..5ea6da64 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -51,7 +51,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
type cooking_info = {
modlist : work_list;
- abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t }
+ abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
(* The type has two caveats:
1) cook_constr is defined after