diff options
| author | Hendrik Tews | 2019-08-20 23:02:33 +0200 |
|---|---|---|
| committer | Hendrik Tews | 2019-08-21 08:38:33 +0200 |
| commit | 4f46b3ff3c904663c99457fbe1ed1a63a5e739b2 (patch) | |
| tree | 08a582677df7611dfdb2618666da36f11b4d40be /pgshell/example.pgsh | |
| parent | aa36785c6e7166da0720e05ba708cdf22687a9d9 (diff) | |
coq-par-compile: fix 8.10 -schedule-vio2vo incompatibility
Use coqc for vio2vo compilation instead of coqtop for
Coq >= 8.10+alpha.
With https://github.com/coq/coq/pull/8690 vio2vo
compilation (-schedule-vio2vo) was moved from coqtop to coqc, see
also https://github.com/coq/coq/issues/10679. This commit makes
PG compilation compatible with Coq after that PR. However, the
patch only checks for the Coq version, therefore making PG vio2vo
compilation fail on 8.10 versions before PR 8690. (Compilation
still works, it's just that vio2vo postprocessing for the mode
quick-and-vio2vo fails.)
Diffstat (limited to 'pgshell/example.pgsh')
0 files changed, 0 insertions, 0 deletions