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 /library/global.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 'library/global.ml')
| -rw-r--r-- | library/global.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/library/global.ml b/library/global.ml index 3f30a63808..44e4a9b7e1 100644 --- a/library/global.ml +++ b/library/global.ml @@ -139,9 +139,14 @@ let body_of_constant_body access env cb = | Undef _ | Primitive _ -> None | Def c -> - Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb) + let u = match cb.const_universes with + | Monomorphic _ -> Opaqueproof.PrivateMonomorphic () + | Polymorphic _ -> Opaqueproof.PrivatePolymorphic Univ.ContextSet.empty + in + Some (Mod_subst.force_constr c, u, Declareops.constant_polymorphic_context cb) | OpaqueDef o -> - Some (Opaqueproof.force_proof access otab o, Declareops.constant_polymorphic_context cb) + let c, u = Opaqueproof.force_proof access otab o in + Some (c, u, Declareops.constant_polymorphic_context cb) let body_of_constant_body access ce = body_of_constant_body access (env ()) ce |