(** 

  This test file should run smoothly if you have Coq 8.18.

  You only need to make sure you can interpret the whole file, not understand
  it.

**)

(* Testing a new feature of 8.18 *)
#[deprecated(note="not really")] Definition foo := 1.

(* Testing that the Coq standard library is found correctly *)
From Coq Require Import Lia.