diff options
| author | Pierre-Marie Pédrot | 2019-06-10 12:27:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-17 15:20:03 +0200 |
| commit | a69bb15b1d76b71628b61bc42eb8d79c098074a8 (patch) | |
| tree | 942ea34a92f2eebf7a442288546233b25065856a /checker | |
| parent | 5316d205993bb3fe3f69e8984fe53d4d50aa8d2a (diff) | |
Merge universe quantification and delayed constraints in opaque proofs.
This enforces more invariants statically.
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/mod_checking.ml | 4 | ||||
| -rw-r--r-- | checker/values.ml | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 7e49e741ad..9b41fbcb7a 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -10,7 +10,7 @@ open Environ let indirect_accessor = ref { Opaqueproof.access_proof = (fun _ _ -> assert false); - Opaqueproof.access_discharge = (fun _ _ _ -> assert false); + Opaqueproof.access_discharge = (fun _ _ -> assert false); } let set_indirect_accessor f = indirect_accessor := f @@ -39,7 +39,7 @@ let check_constant_declaration env kn cb = let c, u = Opaqueproof.force_proof !indirect_accessor otab o in let env' = match u, cb.const_universes with | Opaqueproof.PrivateMonomorphic (), Monomorphic _ -> env' - | Opaqueproof.PrivatePolymorphic local, Polymorphic _ -> + | Opaqueproof.PrivatePolymorphic (_, local), Polymorphic _ -> push_subgraph local env' | _ -> assert false in diff --git a/checker/values.ml b/checker/values.ml index 7b869cd130..9f1baa4d37 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -399,8 +399,8 @@ let v_cooking_info = Tuple ("cooking_info", [|v_work_list; v_abstract|]) let v_delayed_universes = - Sum ("delayed_universes", 0, [| [| v_unit |]; [| v_context_set |] |]) + Sum ("delayed_universes", 0, [| [| v_unit |]; [| Int; v_context_set |] |]) -let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Int; Opt (v_pair v_constr v_delayed_universes) |])) +let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Opt (v_pair v_constr v_delayed_universes) |])) let v_univopaques = Opt (Tuple ("univopaques",[|v_context_set;v_bool|])) |