coq/ex/test-cases/retract-completely-asserted/c.v


1
2
3
4
5
6
7
8
9

Require Import a.
Require Import b.

(* b.a hides a.a, therefore the partial name "a" refers to b.a *)
Print a.

(* a.a is available under its longer name *)
Print a.a.