diff options
| author | Matthieu Sozeau | 2016-09-28 17:26:14 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-10-20 17:39:00 +0200 |
| commit | 474a58b15ca41f1b3287ef3e29e80cca9988598c (patch) | |
| tree | 52446a501765d6185a9b42e737f3d3f7c6ef2b18 /kernel/cemitcodes.ml | |
| parent | 8e0f29cb69f06b64d74b18b09fb6a717034f1140 (diff) | |
Fix bug #5036 autorewrite, sections and universes
Universe context not properly declared. Improve API
and code in declare.ml to allow declaration of universe contexts,
used by declaration of universes and constraints (separately).
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions