summaryrefslogtreecommitdiff
path: root/test-suite/success/CompatOldFlag.v
blob: b7bbc505b488251a011af0868ae15bd0917bbe5a (plain)
1
2
3
4
5
(* -*- coq-prog-args: ("-compat" "8.6") -*- *)
(** Check that the current-minus-two compatibility flag actually requires the relevant modules. *)
Import Coq.Compat.Coq88.
Import Coq.Compat.Coq87.
Import Coq.Compat.Coq86.