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 /kernel/declareops.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 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index de9a052096..a8ebed2326 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -113,7 +113,6 @@ let subst_const_body sub cb = const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; - const_private_poly_univs = cb.const_private_poly_univs; const_relevance = cb.const_relevance; const_inline_code = cb.const_inline_code; const_typing_flags = cb.const_typing_flags } @@ -144,16 +143,11 @@ let hcons_universes cbu = | Polymorphic ctx -> Polymorphic (Univ.hcons_abstract_universe_context ctx) -let hcons_const_private_univs = function - | None -> None - | Some univs -> Some (Univ.hcons_universe_context_set univs) - let hcons_const_body cb = { cb with const_body = hcons_const_def cb.const_body; const_type = Constr.hcons cb.const_type; const_universes = hcons_universes cb.const_universes; - const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs; } (** {6 Inductive types } *) |