summaryrefslogtreecommitdiff
path: root/test-suite/success/CompatOldFlag.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/CompatOldFlag.v')
-rw-r--r--test-suite/success/CompatOldFlag.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v
index b7bbc505..37d50ee6 100644
--- a/test-suite/success/CompatOldFlag.v
+++ b/test-suite/success/CompatOldFlag.v
@@ -1,5 +1,5 @@
-(* -*- coq-prog-args: ("-compat" "8.6") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.7") -*- *)
(** Check that the current-minus-two compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq89.
Import Coq.Compat.Coq88.
Import Coq.Compat.Coq87.
-Import Coq.Compat.Coq86.