diff options
author | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
tree | 0c647056de1832cf1dba5ba58758b9121418e4be /contrib/setoid_ring | |
parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'contrib/setoid_ring')
-rw-r--r-- | contrib/setoid_ring/Field_theory.v | 1 | ||||
-rw-r--r-- | contrib/setoid_ring/InitialRing.v | 10 | ||||
-rw-r--r-- | contrib/setoid_ring/Ring_theory.v | 2 | ||||
-rw-r--r-- | contrib/setoid_ring/ZArithRing.v | 2 | ||||
-rw-r--r-- | contrib/setoid_ring/newring.ml4 | 15 |
5 files changed, 13 insertions, 17 deletions
diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v index 65a397ac..b2e5cc4b 100644 --- a/contrib/setoid_ring/Field_theory.v +++ b/contrib/setoid_ring/Field_theory.v @@ -1619,6 +1619,7 @@ split. generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto. apply H0. generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto. +clear get_sign get_sign_spec. generalize Hp; case l0; simpl; intuition. Qed. diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v index c1fa963f..e664b3b7 100644 --- a/contrib/setoid_ring/InitialRing.v +++ b/contrib/setoid_ring/InitialRing.v @@ -38,14 +38,6 @@ Proof. exact Zmult_plus_distr_l. trivial. exact Zminus_diag. Qed. - Lemma Zeqb_ok : forall x y, Zeq_bool x y = true -> x = y. - Proof. - intros x y. - assert (H := Zcompare_Eq_eq x y);unfold Zeq_bool; - destruct (Zcompare x y);intros H1;auto;discriminate H1. - Qed. - - (** Two generic morphisms from Z to (abrbitrary) rings, *) (**second one is more convenient for proofs but they are ext. equal*) Section ZMORPHISM. @@ -174,7 +166,7 @@ Section ZMORPHISM. Zeq_bool x y = true -> [x] == [y]. Proof. intros x y H. - assert (H1 := Zeqb_ok x y H);unfold IDphi in H1. + assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1. rewrite H1;rrefl. Qed. diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v index 29feab5c..531ab3ca 100644 --- a/contrib/setoid_ring/Ring_theory.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -494,7 +494,7 @@ Qed. Proof. intros;mrewrite. Qed. Lemma ARdistr_r : forall x y z, z * (x + y) == z*x + z*y. - Proof. + Proof. intros;mrewrite. repeat rewrite (ARth.(ARmul_comm) z);sreflexivity. Qed. diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v index 4a5b623b..942915ab 100644 --- a/contrib/setoid_ring/ZArithRing.v +++ b/contrib/setoid_ring/ZArithRing.v @@ -50,7 +50,7 @@ Ltac Zpower_neg := end. Add Ring Zr : Zth - (decidable Zeqb_ok, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc], + (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc], power_tac Zpower_theory [Zpow_tac], (* The two following option are not needed, it is the default chose when the set of coefficiant is usual ring Z *) diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index dd79801d..3d022add 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id: newring.ml4 11094 2008-06-10 19:35:23Z herbelin $ i*) +(*i $Id: newring.ml4 11282 2008-07-28 11:51:53Z msozeau $ i*) open Pp open Util @@ -452,11 +452,14 @@ let (theory_to_obj, obj_to_theory) = let setoid_of_relation env a r = - lapp coq_mk_Setoid - [|a ; r ; - Class_tactics.reflexive_proof env a r ; - Class_tactics.symmetric_proof env a r ; - Class_tactics.transitive_proof env a r |] + try + lapp coq_mk_Setoid + [|a ; r ; + Class_tactics.reflexive_proof env a r ; + Class_tactics.symmetric_proof env a r ; + Class_tactics.transitive_proof env a r |] + with Not_found -> + error "cannot find setoid relation" let op_morph r add mul opp req m1 m2 m3 = lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |] |