summaryrefslogtreecommitdiff
path: root/test-suite/success/import_lib.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/import_lib.v')
-rw-r--r--test-suite/success/import_lib.v50
1 files changed, 25 insertions, 25 deletions
diff --git a/test-suite/success/import_lib.v b/test-suite/success/import_lib.v
index c3dc2fc6..fcedb2b1 100644
--- a/test-suite/success/import_lib.v
+++ b/test-suite/success/import_lib.v
@@ -1,8 +1,8 @@
Definition le_trans := 0.
-Module Test_Read.
- Module M.
+Module Test_Read.
+ Module M.
Require Le. (* Reading without importing *)
Check Le.le_trans.
@@ -12,7 +12,7 @@ Module Test_Read.
Qed.
End M.
- Check Le.le_trans.
+ Check Le.le_trans.
Lemma th0 : le_trans = 0.
reflexivity.
@@ -32,84 +32,84 @@ Definition le_decide := 1. (* from Arith/Compare *)
Definition min := 0. (* from Arith/Min *)
Module Test_Require.
-
+
Module M.
Require Import Compare. (* Imports Min as well *)
-
+
Lemma th1 : le_decide = le_decide.
reflexivity.
Qed.
-
+
Lemma th2 : min = min.
reflexivity.
Qed.
-
+
End M.
-
+
(* Checks that Compare and List are loaded *)
Check Compare.le_decide.
Check Min.min.
-
-
+
+
(* Checks that Compare and List are _not_ imported *)
Lemma th1 : le_decide = 1.
reflexivity.
Qed.
-
+
Lemma th2 : min = 0.
reflexivity.
Qed.
-
+
(* It should still be the case after Import M *)
Import M.
-
+
Lemma th3 : le_decide = 1.
reflexivity.
Qed.
-
+
Lemma th4 : min = 0.
reflexivity.
Qed.
-End Test_Require.
+End Test_Require.
(****************************************************************)
Module Test_Import.
Module M.
Import Compare. (* Imports Min as well *)
-
+
Lemma th1 : le_decide = le_decide.
reflexivity.
Qed.
-
+
Lemma th2 : min = min.
reflexivity.
Qed.
-
+
End M.
-
+
(* Checks that Compare and List are loaded *)
Check Compare.le_decide.
Check Min.min.
-
-
+
+
(* Checks that Compare and List are _not_ imported *)
Lemma th1 : le_decide = 1.
reflexivity.
Qed.
-
+
Lemma th2 : min = 0.
reflexivity.
Qed.
-
+
(* It should still be the case after Import M *)
Import M.
-
+
Lemma th3 : le_decide = 1.
reflexivity.
Qed.
-
+
Lemma th4 : min = 0.
reflexivity.
Qed.