diff options
Diffstat (limited to 'kernel/opaqueproof.ml')
| -rw-r--r-- | kernel/opaqueproof.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 102dcf99f..673b12b2c 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -7,11 +7,16 @@ (************************************************************************) open Names +open Univ open Term open Mod_subst -type work_list = Id.t array Cmap.t * Id.t array Mindmap.t -type cooking_info = { modlist : work_list; abstract : Context.named_context } +type work_list = (Instance.t * Id.t array) Cmap.t * + (Instance.t * Id.t array) Mindmap.t + +type cooking_info = { + modlist : work_list; + abstract : Context.named_context in_universe_context } type proofterm = (constr * Univ.constraints) Future.computation type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) @@ -94,7 +99,7 @@ let force_constraints = function | NoIndirect(_,cu) -> snd(Future.force cu) | Indirect (_,dp,i) -> match !get_univ dp i with - | None -> Univ.empty_constraint + | None -> Univ.Constraint.empty | Some u -> Future.force u let get_constraints = function |