aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/CompatOldOldFlag.v
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-11-21 18:49:30 +0100
committerEmilio Jesus Gallego Arias2019-11-27 13:53:50 +0100
commitcec1688022638679300af01c56fc6af908ae0681 (patch)
treecfea3dae638de4f9a9774ac6e0bc6b8e8fab9c7d /test-suite/success/CompatOldOldFlag.v
parent90aadb2697884e9ee42f0a1828568ca9dad3f85e (diff)
[release] Update files for 8.12 release per release process.
Diffstat (limited to 'test-suite/success/CompatOldOldFlag.v')
-rw-r--r--test-suite/success/CompatOldOldFlag.v6
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v
new file mode 100644
index 0000000000..dd259988ac
--- /dev/null
+++ b/test-suite/success/CompatOldOldFlag.v
@@ -0,0 +1,6 @@
+(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
+(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq812.
+Import Coq.Compat.Coq811.
+Import Coq.Compat.Coq810.
+Import Coq.Compat.Coq89.