diff options
Diffstat (limited to 'test-suite/modules/modul.v')
| -rw-r--r-- | test-suite/modules/modul.v | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v index 5612ea7553..58ae2a52df 100644 --- a/test-suite/modules/modul.v +++ b/test-suite/modules/modul.v @@ -16,24 +16,22 @@ Module M. End M. +Locate Module M. + (*Lemma w1 : (M.rel O (S O)). Auto. *) Import M. -Print Hint *. Lemma w1 : (O#(S O)). -Print Hint. -Print Hint *. - Auto. Save. Check (O#O). Locate rel. -Locate M. +Locate Module M. Module N:=Top.M. |