summaryrefslogtreecommitdiff
path: root/test-suite/success/CompatPreviousFlag.v
blob: 99813883814a7bca440e32305212fd147a141d7b (plain)
1
2
3
4
(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
(** Check that the current-minus-one compatibility flag actually requires the relevant modules. *)
Import Coq.Compat.Coq89.
Import Coq.Compat.Coq88.