2 files changed, 16 insertions, 2 deletions
diff --git a/plugins/setoid_ring/Cring_tac.v b/plugins/setoid_ring/Cring_tac.v
index 8df45b56e..c7f0ae779 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 15dad95e1..c4dfe3169 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