coq/ex/test-cases/stale-load-path/c/c.v


1
2
3
4
5
6
7
8
9

(* This file depends on Coq.Arith.Le from the standard library. *)

Require Le.

(* The next print should work. *)
Print Le.le_refl.

(* The next print should not work. *)
Print Le.a.