diff options
Diffstat (limited to 'coq/ex/test-cases/retract-completely-asserted/c.v')
| -rw-r--r-- | coq/ex/test-cases/retract-completely-asserted/c.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/coq/ex/test-cases/retract-completely-asserted/c.v b/coq/ex/test-cases/retract-completely-asserted/c.v new file mode 100644 index 00000000..bd82b351 --- /dev/null +++ b/coq/ex/test-cases/retract-completely-asserted/c.v @@ -0,0 +1,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.
\ No newline at end of file |