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/values.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/values.ml')
| -rw-r--r-- | checker/values.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/checker/values.ml b/checker/values.ml index 4a4c8d803c..7b869cd130 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -230,7 +230,6 @@ let v_cb = v_tuple "constant_body" v_relevance; Any; v_univs; - Opt v_context_set; v_bool; v_typing_flags|] @@ -399,6 +398,9 @@ let v_abstract = let v_cooking_info = Tuple ("cooking_info", [|v_work_list; v_abstract|]) -let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Int; Opt v_constr |])) +let v_delayed_universes = + Sum ("delayed_universes", 0, [| [| v_unit |]; [| v_context_set |] |]) + +let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Int; Opt (v_pair v_constr v_delayed_universes) |])) let v_univopaques = Opt (Tuple ("univopaques",[|v_context_set;v_bool|])) |