aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/CompatOldOldFlag.v
blob: 1f62635f50a84e34b619cd15454ff76e314b89e4 (plain)
1
2
3
4
5
6
(* -*- coq-prog-args: ("-compat" "8.7") -*- *)
(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
Import Coq.Compat.Coq810.
Import Coq.Compat.Coq89.
Import Coq.Compat.Coq88.
Import Coq.Compat.Coq87.