aboutsummaryrefslogtreecommitdiff
path: root/dev/header.py
diff options
context:
space:
mode:
authorJason Gross2020-04-28 21:05:39 -0400
committerJason Gross2020-05-09 13:39:27 -0400
commit3c66c60e52b334482bcfe3d1d97bb77e4d011d18 (patch)
tree62c4f112b894c37b302263f11b66b258be88d466 /dev/header.py
parent573fed5a9060b8ebfed5bcf9ee573c928449119a (diff)
[with_strategy] Fix for coqchk
We need to record the transparency information in the libobject stack in order for coqchk to not trip over the strategy information. This is quite sketchy, though.
Diffstat (limited to 'dev/header.py')
0 files changed, 0 insertions, 0 deletions