diff options
| author | Pierre-Marie Pédrot | 2018-09-27 15:34:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-09 14:10:27 +0100 |
| commit | 168af2ba6ae1facf948c7c7bee725ac0f0cd3b41 (patch) | |
| tree | 3953f4716691915cd393ee3640e3cf6770d62701 /vernac/comProgramFixpoint.ml | |
| parent | 601ce3738253e4bb197900ee6dad271c4e3666d6 (diff) | |
Force the user to provide names when generating abstract universe contexts.
For now this data is not stored, but the code checks that indeed the number
of names provided coincide with the instance length.
I had to reimplement the same kind of workaround hack in section handling as
the one already performed in UnivNames because the name information is not
present in the section data structure. This deserves a FIXME.
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions
