test-suite/success/CompatPreviousFlag.v


1
2
3
4

(* -*- coq-prog-args: ("-compat" "8.11") -*- *)
(** Check that the current-minus-one compatibility flag actually requires the relevant modules. *)
Import Coq.Compat.Coq812.
Import Coq.Compat.Coq811.