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/safe_typing.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/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a0cc2974d9..7526508c4e 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -691,7 +691,7 @@ let constant_entry_of_side_effect eff = if Declareops.is_opaque cb then OpaqueEntry { opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); - opaque_entry_secctx = None; + opaque_entry_secctx = cb.const_hyps; opaque_entry_feedback = None; opaque_entry_type = cb.const_type; opaque_entry_universes = univs; @@ -699,7 +699,7 @@ let constant_entry_of_side_effect eff = else DefinitionEntry { const_entry_body = (p, Univ.ContextSet.empty); - const_entry_secctx = None; + const_entry_secctx = Some cb.const_hyps; const_entry_feedback = None; const_entry_type = Some cb.const_type; const_entry_universes = univs; |