From da1e32cbdc78050ea2e89eee896ba2b40db1b5dd Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sun, 3 Apr 2011 11:23:25 +0000
Subject: Quickly avoid global axioms in Loic new files about ring

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13951 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/setoid_ring/Cring_tac.v | 9 ++++++++-
 plugins/setoid_ring/Ring2_tac.v | 9 ++++++++-
 2 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/plugins/setoid_ring/Cring_tac.v b/plugins/setoid_ring/Cring_tac.v
index 8df45b56e7..c7f0ae7791 100644
--- a/plugins/setoid_ring/Cring_tac.v
+++ b/plugins/setoid_ring/Cring_tac.v
@@ -207,6 +207,12 @@ Ltac cring:=
           cring_gen; cring_compute
   end.
 
+(* Pierre L: these tests should be done in a section, otherwise
+   global axioms are generated. Ideally such tests should go in
+   the test-suite directory *)
+
+Section Tests.
+
 (* Tests *)
 
 Variable R: Type.
@@ -221,7 +227,7 @@ Qed.
 sinon, le reste de la tactique donne le même temps que ring 
 *)
 Goal forall x y z  t u :R, (x + y + z + t + u)^13 == (u + t + z + y + x) ^13.
-Time cring. (*Finished transaction in 0. secs (0.410938u,0.s)*)
+(*Time*) cring. (*Finished transaction in 0. secs (0.410938u,0.s)*)
 Qed.
 (*
 Goal forall x y z  t u :R, (x + y + z + t + u)^16 == (u + t + z + y + x) ^16.
@@ -264,3 +270,4 @@ cring.
 Qed.
 *)
 
+End Tests.
\ No newline at end of file
diff --git a/plugins/setoid_ring/Ring2_tac.v b/plugins/setoid_ring/Ring2_tac.v
index 15dad95e19..c4dfe31690 100644
--- a/plugins/setoid_ring/Ring2_tac.v
+++ b/plugins/setoid_ring/Ring2_tac.v
@@ -156,6 +156,11 @@ Lemma Zeqb_ok: forall x y : Z, Zeq_bool x y = true -> x == y.
            end
        end
    end.
+
+(* Pierre L: these tests should be done in a section, otherwise
+   global axioms are generated. Ideally such tests should go in
+   the test-suite directory *)
+Section Tests.
  
 Ltac ring2:= 
   unset_ring_notations; intros;
@@ -187,4 +192,6 @@ Qed.
 (* Fails with Multiplication: A -> B -> C.
 Goal forall x:R,    2%Z * (x * x) == 3%Z * x.
 Admitted.
-*)
\ No newline at end of file
+*)
+
+End Tests.
\ No newline at end of file
-- 
cgit v1.2.3