From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 test-suite/success/import_lib.v | 122 ++++++++++++++++++++--------------------
 1 file changed, 61 insertions(+), 61 deletions(-)

(limited to 'test-suite/success/import_lib.v')

diff --git a/test-suite/success/import_lib.v b/test-suite/success/import_lib.v
index d031691d..c3dc2fc6 100644
--- a/test-suite/success/import_lib.v
+++ b/test-suite/success/import_lib.v
@@ -1,47 +1,47 @@
-Definition le_trans:=O.
+Definition le_trans := 0.
 
 
 Module Test_Read.     
   Module M.  
-    Read Module Le.        (* Reading without importing *)
+    Require Le.        (* Reading without importing *)
 
     Check Le.le_trans.
 
-    Lemma th0 : le_trans = O.
-      Reflexivity.
+    Lemma th0 : le_trans = 0.
+      reflexivity.
     Qed.
   End M.
 
   Check Le.le_trans. 
 
-  Lemma th0 : le_trans = O.
-    Reflexivity.
+  Lemma th0 : le_trans = 0.
+    reflexivity.
   Qed.
 
   Import M.
 
-  Lemma th1 : le_trans = O.
-    Reflexivity.
+  Lemma th1 : le_trans = 0.
+    reflexivity.
   Qed.
 End Test_Read.
 
 
 (****************************************************************)
 
-Definition le_decide := (S O).  (* from Arith/Compare *)
-Definition min := O.            (* from Arith/Min *)
+Definition le_decide := 1.  (* from Arith/Compare *)
+Definition min := 0.            (* from Arith/Min *)
 
 Module Test_Require.
   
   Module M.
-    Require Compare.              (* Imports Min as well *)
+    Require Import Compare.              (* Imports Min as well *)
   
-    Lemma th1 : le_decide = Compare.le_decide.
-      Reflexivity.
+    Lemma th1 : le_decide = le_decide.
+      reflexivity.
     Qed.
   
-    Lemma th2 : min = Min.min.
-      Reflexivity.
+    Lemma th2 : min = min.
+      reflexivity.
     Qed.
   
   End M.
@@ -52,23 +52,23 @@ Module Test_Require.
   
   
   (* Checks that Compare and List are _not_ imported *)
-  Lemma th1 : le_decide = (S O).
-    Reflexivity.
+  Lemma th1 : le_decide = 1.
+    reflexivity.
   Qed.
   
-  Lemma th2 : min = O.
-    Reflexivity.
+  Lemma th2 : min = 0.
+    reflexivity.
   Qed.
   
   (* It should still be the case after Import M *)
   Import M.
   
-  Lemma th3 : le_decide = (S O).
-    Reflexivity.
+  Lemma th3 : le_decide = 1.
+    reflexivity.
   Qed.
   
-  Lemma th4 : min = O.
-    Reflexivity.
+  Lemma th4 : min = 0.
+    reflexivity.
   Qed.
 
 End Test_Require.  
@@ -79,12 +79,12 @@ Module Test_Import.
   Module M.
     Import Compare.              (* Imports Min as well *)
   
-    Lemma th1 : le_decide = Compare.le_decide.
-      Reflexivity.
+    Lemma th1 : le_decide = le_decide.
+      reflexivity.
     Qed.
   
-    Lemma th2 : min = Min.min.
-      Reflexivity.
+    Lemma th2 : min = min.
+      reflexivity.
     Qed.
   
   End M.
@@ -95,23 +95,23 @@ Module Test_Import.
   
   
   (* Checks that Compare and List are _not_ imported *)
-  Lemma th1 : le_decide = (S O).
-    Reflexivity.
+  Lemma th1 : le_decide = 1.
+    reflexivity.
   Qed.
   
-  Lemma th2 : min = O.
-    Reflexivity.
+  Lemma th2 : min = 0.
+    reflexivity.
   Qed.
   
   (* It should still be the case after Import M *)
   Import M.
   
-  Lemma th3 : le_decide = (S O).
-    Reflexivity.
+  Lemma th3 : le_decide = 1.
+    reflexivity.
   Qed.
   
-  Lemma th4 : min = O.
-    Reflexivity.
+  Lemma th4 : min = 0.
+    reflexivity.
   Qed.
 End Test_Import.
 
@@ -121,24 +121,24 @@ Module Test_Export.
   Module M.
     Export Compare.              (* Exports Min as well *)
 
-    Lemma th1 : le_decide = Compare.le_decide.
-      Reflexivity.
+    Lemma th1 : le_decide = le_decide.
+      reflexivity.
     Qed.
 
-    Lemma th2 : min = Min.min.
-      Reflexivity.
+    Lemma th2 : min = min.
+      reflexivity.
     Qed.
 
   End M.
 
 
   (* Checks that Compare and List are _not_ imported *)
-  Lemma th1 : le_decide = (S O).
-    Reflexivity.
+  Lemma th1 : le_decide = 1.
+    reflexivity.
   Qed.
 
-  Lemma th2 : min = O.
-    Reflexivity.
+  Lemma th2 : min = 0.
+    reflexivity.
   Qed.
 
 
@@ -146,12 +146,12 @@ Module Test_Export.
 
   Import M.
 
-  Lemma th3 : le_decide = Compare.le_decide.
-    Reflexivity.
+  Lemma th3 : le_decide = le_decide.
+    reflexivity.
   Qed.
 
-  Lemma th4 : min = Min.min.
-    Reflexivity.
+  Lemma th4 : min = min.
+    reflexivity.
   Qed.
 End Test_Export.
 
@@ -160,30 +160,30 @@ End Test_Export.
 
 Module Test_Require_Export.
 
-  Definition mult_sym:=(S O).    (* from Arith/Mult *)
-  Definition plus_sym:=O.        (* from Arith/Plus *)
+  Definition mult_sym := 1.    (* from Arith/Mult *)
+  Definition plus_sym := 0.        (* from Arith/Plus *)
 
   Module M.
     Require Export Mult.         (* Exports Plus as well *)
 
-    Lemma th1 : mult_sym = Mult.mult_sym.
-      Reflexivity.
+    Lemma th1 : mult_comm = mult_comm.
+      reflexivity.
     Qed.
 
-    Lemma th2 : plus_sym = Plus.plus_sym.
-      Reflexivity.
+    Lemma th2 : plus_comm = plus_comm.
+      reflexivity.
     Qed.
 
   End M.
 
 
   (* Checks that Mult and Plus are _not_ imported *)
-  Lemma th1 : mult_sym = (S O).
-    Reflexivity.
+  Lemma th1 : mult_sym = 1.
+    reflexivity.
   Qed.
 
-  Lemma th2 : plus_sym = O.
-    Reflexivity.
+  Lemma th2 : plus_sym = 0.
+    reflexivity.
   Qed.
 
 
@@ -191,12 +191,12 @@ Module Test_Require_Export.
 
   Import M.
 
-  Lemma th3 : mult_sym = Mult.mult_sym.
-    Reflexivity.
+  Lemma th3 : mult_comm = mult_comm.
+    reflexivity.
   Qed.
 
-  Lemma th4 : plus_sym = Plus.plus_sym.
-    Reflexivity.
+  Lemma th4 : plus_comm = plus_comm.
+    reflexivity.
   Qed.
 
 End Test_Require_Export.
-- 
cgit v1.2.3