diff options
| author | Pierre-Marie Pédrot | 2021-01-11 16:41:19 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-11 16:52:10 +0100 |
| commit | 3c427cd52ad7e41b4a8cbb7e227b8f79730863b1 (patch) | |
| tree | 8b9de51ec0317b812c3bc873b72dd54310e03022 /vernac/comProgramFixpoint.mli | |
| parent | 76de13a9ce03f542bca74dabee28bf27d9d8ac4f (diff) | |
Do not declare a global universe object when the universe set is empty.
Diffstat (limited to 'vernac/comProgramFixpoint.mli')
0 files changed, 0 insertions, 0 deletions