aboutsummaryrefslogtreecommitdiff
path: root/generic
diff options
context:
space:
mode:
authorClément Pit--Claudel2017-02-25 19:44:25 -0500
committerClément Pit--Claudel2017-03-08 15:06:17 -0500
commit031a5780575f3b87124df303b42e202aa5e1c418 (patch)
tree3796e148d9964a18fc7984a92e0b626ab313a6c8 /generic
parent98f2e463287e3562dc7b7126e062919a8604ca4a (diff)
easycrypt: Don't require pg-custom: it breaks compilation
The problem is that loading pg-custom runs a bunch of defpgcustom, with no current proof assistant. Then when coq or easycrypt calls proof-ready-for-assistant, pg-custom isn't loaded again.
Diffstat (limited to 'generic')
0 files changed, 0 insertions, 0 deletions