diff options
| author | Gaëtan Gilbert | 2019-06-27 13:36:39 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-27 13:41:45 +0200 |
| commit | 5a532f2e00d0e3dca8d7079f067c79f2bb1b6b14 (patch) | |
| tree | 55913a55662e73353f360d90baa7eff6e59e3867 /kernel/safe_typing.ml | |
| parent | b7c85c2ebe8375232719cd2d61e55daef9b4a358 (diff) | |
Kernel transparent definition entries have no body universes.
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 7526508c4e..2c434d4edf 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -698,7 +698,7 @@ let constant_entry_of_side_effect eff = } else DefinitionEntry { - const_entry_body = (p, Univ.ContextSet.empty); + const_entry_body = p; const_entry_secctx = Some cb.const_hyps; const_entry_feedback = None; const_entry_type = Some cb.const_type; |