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/entries.ml | |
| 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/entries.ml')
| -rw-r--r-- | kernel/entries.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 1e6bc14935..8c4bd16ae3 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -102,11 +102,10 @@ type 'a const_entry_body = 'a proof_output Future.computation (** Dummy wrapper type discriminable from unit *) type 'a seff_wrap = { seff_wrap : 'a } -type _ constant_entry = - | DefinitionEntry : definition_entry -> unit constant_entry - | OpaqueEntry : 'a const_entry_body opaque_entry -> 'a seff_wrap constant_entry - | ParameterEntry : parameter_entry -> unit constant_entry - | PrimitiveEntry : primitive_entry -> unit constant_entry +type constant_entry = + | DefinitionEntry : definition_entry -> constant_entry + | ParameterEntry : parameter_entry -> constant_entry + | PrimitiveEntry : primitive_entry -> constant_entry (** {6 Modules } *) |