aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/CompatCurrentFlag.v
AgeCommit message (Collapse)Author
2020-11-23Update compat infrastructure for 8.14Enrico Tassi
2020-05-18Update to 8.13.Théo Zimmermann
Part of this PR was automatically generated by running dev/doc/update-compat.py --master
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-10-07Call to update-compat.py.Pierre-Marie Pédrot
2019-01-24Update -compat to support -compat 8.10Jason Gross
This commit was created via `./dev/tools/update-compat.py --master`
2018-10-02Update the -compat flagsJason Gross
Mostly via `dev/tools/update-compat.py --cur-version=8.9` We just remove test-suite/success/FunindExtraction_compat86.v because, except for the `Extraction iszero.` line at the bottom, it is a duplicate of `test-suite/success/Funind.v` (except with `-compat 8.6`). We also manually update a number of test-suite files to pre-emptively remove compatibility notations (which used to be compat 8.6, but are now compat 8.7).
2018-09-02Make -compat 8.8 import Coq.Compat.Coq88Jason Gross
Fixes #8311