diff options
| author | Pierre-Marie Pédrot | 2019-06-28 22:04:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-16 17:38:49 +0200 |
| commit | 1f2a3fe97be66fd3201b9c98e5744953d4149b91 (patch) | |
| tree | 9e1e992d5f2f706505e4184d990f2790e41df6ca /kernel/safe_typing.mli | |
| parent | f22205ee06f9170a74dc8cefba2b42deeaeb246b (diff) | |
Cleaning up the previous code by ensuring statically invariants on opaque proofs.
We return the typing context directly instead of hiding it into the opaque
data, and we take advantage of this to remove a few assertions known to hold
statically.
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 1b55293f1c..6e5c9c55ae 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -78,7 +78,8 @@ type 'a effect_entry = | PureEntry : unit effect_entry type global_declaration = - | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration +| ConstantEntry : Entries.constant_entry -> global_declaration +| OpaqueEntry : private_constants Entries.const_entry_body Entries.opaque_entry -> global_declaration type exported_private_constant = Constant.t |