diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-03 11:23:25 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-03 11:23:25 +0000 |
commit | da1e32cbdc78050ea2e89eee896ba2b40db1b5dd (patch) | |
tree | 5f247a7df0d8a7329af8470ca34e72273d922f27 | |
parent | f1bd9d023a01ff064e2d1080a081d7ec178df9a1 (diff) |
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
-rw-r--r-- | plugins/setoid_ring/Cring_tac.v | 9 | ||||
-rw-r--r-- | 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 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 |