diff options
| author | Pierre-Marie Pédrot | 2019-06-24 19:05:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-26 12:38:27 +0200 |
| commit | 64e66fd019b968f863a80d4bce972545a66ea966 (patch) | |
| tree | 97d120af900084eb7e4113c44e9372ee6a9defa8 /kernel/entries.ml | |
| parent | 6fab6f1cbf21d6f4a3a77e1b73c31fbe18d05a11 (diff) | |
Perform the opaque section variable inference outside of the kernel.
It is not the role of the kernel to decide to force the body of an entry
to infer the section variable it uses, but the one of the upper layers.
We make this explicit in the type of entries so as to enforce that this
inference is performed beforehand.
Also removes auxilliary file stuff that doesn't look like it belongs in
the kernel either.
Diffstat (limited to 'kernel/entries.ml')
| -rw-r--r-- | kernel/entries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 2d29c3ee19..ca08ba485e 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -80,7 +80,7 @@ type section_def_entry = { type 'a opaque_entry = { opaque_entry_body : 'a; (* List of section variables *) - opaque_entry_secctx : Constr.named_context option; + opaque_entry_secctx : Constr.named_context; (* State id on which the completion of type checking is reported *) opaque_entry_feedback : Stateid.t option; opaque_entry_type : types; |