ring2, cring, nsatz avec type classe avec parametres plus notations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14175 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 25 deletions

diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
index 518d22e98..acb5cfd19 100644
--- a/test-suite/success/Nsatz.v
+++ b/test-suite/success/Nsatz.v
@@ -2,33 +2,10 @@ Require Import Nsatz ZArith Reals List Ring_polynom.
 
 (* Example with a generic domain *)
 
-Variable A: Type.
-Variable Ad: Domain A.
-
-Definition Ari : Ring A:= (@domain_ring A Ad).
-Existing Instance Ari.
-
-Existing Instance ring_setoid.
-Existing Instance ring_plus_comp.
-Existing Instance ring_mult_comp.
-Existing Instance ring_sub_comp.
-Existing Instance ring_opp_comp.
-
-Add Ring Ar: (@ring_ring A (@domain_ring A Ad)).
-
-Instance zero_ring2 : Zero A := {zero := ring0}.
-Instance one_ring2 : One A := {one := ring1}.
-Instance addition_ring2 : Addition A := {addition x y := ring_plus x y}.
-Instance multiplication_ring2 : Multiplication A := {multiplication x y := ring_mult x y}.
-Instance subtraction_ring2 : Subtraction A := {subtraction x y := ring_sub x y}.
-Instance opposite_ring2 : Opposite A := {opposite x := ring_opp x}.
-
-Infix "==" := ring_eq (at level 70, no associativity).
-
-Ltac nsatzA := simpl; unfold Ari; nsatz_domain.
+Context {R:Type}`{Rid:Integral_domain R}.
 
 Goal forall x y:A,  x == y -> x+0 == y*1+0.
-nsatzA.
+nsatz.
 Qed.
 
 Lemma example3 : forall x y z,