diff options
| author | Pierre-Marie Pédrot | 2019-06-04 13:44:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-17 15:20:02 +0200 |
| commit | 5316d205993bb3fe3f69e8984fe53d4d50aa8d2a (patch) | |
| tree | 8016562d06949b981a3e58e71103b02aea7f1c44 /checker/check.ml | |
| parent | 7e47fea5ce050c8129ba2d6f94e93fbc29763a3b (diff) | |
Allow to delay polymorphic opaque constants.
We had to move the private opaque constraints out of the constant declaration
into the opaque table. The API is not very pretty yet due to a pervasive
confusion between monomorphic global constraints and polymorphic local ones,
but once we get rid of futures in the kernel this should be magically solved.
Diffstat (limited to 'checker/check.ml')
| -rw-r--r-- | checker/check.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/checker/check.ml b/checker/check.ml index 903258daef..89cb834a4a 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -51,7 +51,7 @@ let pr_path sp = type compilation_unit_name = DirPath.t type seg_univ = Univ.ContextSet.t * bool -type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.constr option) array +type seg_proofs = Opaqueproof.opaque_proofterm array type library_t = { library_name : compilation_unit_name; @@ -98,10 +98,7 @@ let access_opaque_table dp i = with Not_found -> assert false in assert (i < Array.length t); - let (info, n, c) = t.(i) in - match c with - | None -> None - | Some c -> Some (Cooking.cook_constr info n c) + t.(i) let access_discharge = Cooking.cook_constr |