aboutsummaryrefslogtreecommitdiff
path: root/vernac/comProgramFixpoint.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-09-27 15:34:28 +0200
committerPierre-Marie Pédrot2018-11-09 14:10:27 +0100
commit168af2ba6ae1facf948c7c7bee725ac0f0cd3b41 (patch)
tree3953f4716691915cd393ee3640e3cf6770d62701 /vernac/comProgramFixpoint.ml
parent601ce3738253e4bb197900ee6dad271c4e3666d6 (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