aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/CompatCurrentFlag.v
blob: fd6101bf89a5c4fc67f159d57b110f73d0b5e316 (plain)
1
2
3
(* -*- coq-prog-args: ("-compat" "8.11") -*- *)
(** Check that the current compatibility flag actually requires the relevant modules. *)
Import Coq.Compat.Coq811.