args implicites dans Field

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

3 files changed, 47 insertions, 47 deletions

diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v
index b16afad8d..eafcb41a7 100644
--- a/contrib/setoid_ring/Field_tac.v
+++ b/contrib/setoid_ring/Field_tac.v
@@ -17,24 +17,24 @@ Require Export Field_theory.
         match t with 
         | (radd ?t1 ?t2) => 
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(FEadd C e1 e2)
+          let e2 := mkP t2 in constr:(FEadd e1 e2)
         | (rmul ?t1 ?t2) => 
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(FEmul C e1 e2)
+          let e2 := mkP t2 in constr:(FEmul e1 e2)
         | (rsub ?t1 ?t2) => 
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(FEsub C e1 e2)
+          let e2 := mkP t2 in constr:(FEsub e1 e2)
         | (ropp ?t1) =>
-          let e1 := mkP t1 in constr:(FEopp C e1)
+          let e1 := mkP t1 in constr:(FEopp e1)
         | (rdiv ?t1 ?t2) => 
           let e1 := mkP t1 in
-          let e2 := mkP t2 in constr:(FEdiv C e1 e2)
+          let e2 := mkP t2 in constr:(FEdiv e1 e2)
         | (rinv ?t1) =>
-          let e1 := mkP t1 in constr:(FEinv C e1)
+          let e1 := mkP t1 in constr:(FEinv e1)
         | _ =>
-          let p := Find_at t fv in constr:(FEX C p)
+          let p := Find_at t fv in constr:(@FEX C p)
         end
-    | ?c => constr:(FEc C c)
+    | ?c => constr:(FEc c)
     end
  in mkP t.
 
@@ -74,21 +74,21 @@ Ltac simpl_PCond req rO :=
   try (exact I);
   fold_field_cond req rO.
 
-(* Rewriting *)
+(* Rewriting (field_simplify) *)
 Ltac Field_rewrite_list lemma Cond_lemma req Cst_tac :=
   let Make_tac :=
     match type of lemma with
     | forall l fe nfe,
       _ = nfe -> 
-      PCond _ _ _ _ _ _ _ _ _ _ _ ->
-      req (FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv ?C ?phi l fe) _ =>
+      PCond _ _ _ _ _ _ _ _ _ ->
+      req (@FEeval ?R ?rO ?radd ?rmul ?rsub ?ropp ?rdiv ?rinv ?C ?phi l fe) _ =>
         let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in
         let mkFE := mkFieldexpr C Cst_tac radd rmul rsub ropp rdiv rinv in
         let simpl_field H := (*protect_fv "field" in H*)
 unfold Pphi_dev in H;simpl in H in 
         (fun f => f mkFV mkFE simpl_field lemma req;
                   try (apply Cond_lemma; simpl_PCond req rO))
-    | _ => fail 1 "field anomaly: bad correctness lemma"
+    | _ => fail 1 "field anomaly: bad correctness lemma (rewr)"
     end in
   Make_tac ReflexiveRewriteTactic.
 (* Pb: second rewrite are applied to non-zero condition of first rewrite... *)
@@ -99,10 +99,10 @@ Ltac Field_Scheme FV_tac SYN_tac SIMPL_tac lemma Cond_lemma req :=
   let ParseLemma :=
     match type of lemma with
     | forall l fe1 fe2 nfe1 nfe2, _ = nfe1 -> _ = nfe2 -> _ -> 
-      PCond _ _ _ _ _ _ _ _ _ _ _ ->
-      req (FEeval ?R ?rO _ _ _ _ _ _ _ _ l fe1) _ =>
+      PCond _ _ _ _ _ _ _ _ _ ->
+      req (@FEeval ?R ?rO _ _ _ _ _ _ _ _ l fe1) _ =>
         (fun f => f R rO)
-    | _ => fail 1 "field anomaly: bad correctness lemma" 
+    | _ => fail 1 "field anomaly: bad correctness lemma (scheme)" 
     end in
   let ParseExpr2 ilemma :=
     match type of ilemma with
@@ -132,14 +132,14 @@ Ltac Field_Scheme FV_tac SYN_tac SIMPL_tac lemma Cond_lemma req :=
 Ltac ParseFieldComponents lemma req :=
   match type of lemma with
   | forall l fe1 fe2 nfe1 nfe2,
-    _ = nfe1 -> _ = nfe2 -> _ -> PCond _ _ _ _ _ _ _ _ _ _ _ ->
-    req (FEeval ?R ?rO ?add ?mul ?sub ?opp ?div ?inv ?C ?phi l fe1) _ =>
+    _ = nfe1 -> _ = nfe2 -> _ -> PCond _ _ _ _ _ _ _ _ _ ->
+    req (@FEeval ?R ?rO ?add ?mul ?sub ?opp ?div ?inv ?C ?phi l fe1) _ =>
       (fun f => f add mul sub opp div inv C)
-  | _ => fail 1 "field: bad correctness lemma"
+  | _ => fail 1 "field anomaly: bad correctness lemma (parse)"
   end.
 
 (* solve completely a field equation, leaving non-zero conditions to be
-   proved *)
+   proved (field) *)
 Ltac Make_field_tac lemma Cond_lemma req Cst_tac :=
   let Main radd rmul rsub ropp rdiv rinv C :=
     let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in
@@ -150,7 +150,7 @@ Ltac Make_field_tac lemma Cond_lemma req Cst_tac :=
   ParseFieldComponents lemma req Main.
 
 (* transforms a field equation to an equivalent (simplified) ring equation,
-   and leaves non-zero conditions to be proved *)
+   and leaves non-zero conditions to be proved (field_simplify_eq) *)
 Ltac Make_field_simplify_eq_tac lemma Cond_lemma req Cst_tac :=
   let Main radd rmul rsub ropp rdiv rinv C :=
     let mkFV := FFV Cst_tac radd rmul rsub ropp rdiv rinv in
diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v
index 469f2537c..b71eb0596 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/contrib/setoid_ring/Field_theory.v
@@ -9,6 +9,7 @@
 Require Ring.
 Import Ring_polynom Ring_theory InitialRing Setoid List.
 Require Import ZArith_base.
+Set Implicit Arguments.
 
 Section MakeFieldPol.
 
@@ -139,8 +140,8 @@ Hint Resolve SRdiv_ext .
 Lemma rmul_reg_l : forall p q1 q2,
   ~ p == 0 -> p * q1 == p * q2 -> q1 == q2.
 intros.
-rewrite <- (rdiv_simpl q1 p) in |- *; trivial.
-rewrite <- (rdiv_simpl q2 p) in |- *; trivial.
+rewrite <- (@rdiv_simpl q1 p) in |- *; trivial.
+rewrite <- (@rdiv_simpl q2 p) in |- *; trivial.
 repeat rewrite rdiv_def in |- *.
 repeat rewrite (ARmul_assoc ARth) in |- *.
 auto.
@@ -913,7 +914,7 @@ Lemma ceqb_rect_complete : forall c1 c2 (A:Type) (x y:A) (P:A->Type),
 Proof.
 intros.
 generalize (fun h => X (morph_eq CRmorph c1 c2 h)).
-generalize (ceqb_complete c1 c2).
+generalize (@ceqb_complete c1 c2).
 case (c1 ?=! c2); auto; intros.
 apply X0.
 red in |- *; intro.
@@ -933,7 +934,7 @@ Theorem PFcons1_fcons_inv:
 intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail).
  simpl in |- *; intros c l1.
    apply ceqb_rect_complete; intros.
-  elim (absurd_PCond_bottom l H0).
+  elim (@absurd_PCond_bottom l H0).
   split; trivial.
     rewrite <- (morph0 CRmorph) in |- *; trivial.
  intros p H p0 H0 l1 H1.
@@ -944,7 +945,7 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; auto; fail).
    apply field_is_integral_domain; trivial.
  simpl in |- *; intros p H l1.
    apply ceqb_rect_complete; intros.
-  elim (absurd_PCond_bottom l H1).
+  elim (@absurd_PCond_bottom l H1).
   destruct (H _ H1).
     split; trivial.
     apply ropp_neq_0; trivial.
@@ -996,13 +997,13 @@ End FieldAndSemiField.
 
 End MakeFieldPol.
 
-  Definition SF2AF R rO rI radd rmul rdiv rinv req Rsth 
-    (sf:semi_field_theory R rO rI radd rmul rdiv rinv req)  :=
-    mk_afield _ _ _ _ _ _ _ _ _ _
-      (SRth_ARth Rsth sf.(SF_SR _ _ _ _ _ _ _ _))
-      sf.(SF_1_neq_0 _ _ _ _ _ _ _ _)
-      sf.(SFdiv_def _ _ _ _ _ _ _ _)
-      sf.(SFinv_l _ _ _ _ _ _ _ _).
+  Definition SF2AF R (rO rI:R) radd rmul rdiv rinv req Rsth 
+    (sf:semi_field_theory rO rI radd rmul rdiv rinv req)  :=
+    mk_afield _ _
+      (SRth_ARth Rsth sf.(SF_SR))
+      sf.(SF_1_neq_0)
+      sf.(SFdiv_def)
+      sf.(SFinv_l).
 
 
 Section Complete.
@@ -1024,11 +1025,11 @@ Section Complete.
 
 Section AlmostField.
 
- Variable AFth : almost_field_theory R rO rI radd rmul rsub ropp rdiv rinv req.
- Let ARth := AFth.(AF_AR _ _ _ _ _ _ _ _ _ _).
- Let rI_neq_rO := AFth.(AF_1_neq_0 _ _ _ _ _ _ _ _ _ _).
- Let rdiv_def := AFth.(AFdiv_def _ _ _ _ _ _ _ _ _ _).
- Let rinv_l := AFth.(AFinv_l _ _ _ _ _ _ _ _ _ _).
+ Variable AFth : almost_field_theory rO rI radd rmul rsub ropp rdiv rinv req.
+ Let ARth := AFth.(AF_AR).
+ Let rI_neq_rO := AFth.(AF_1_neq_0).
+ Let rdiv_def := AFth.(AFdiv_def).
+ Let rinv_l := AFth.(AFinv_l).
 
 Hypothesis S_inj : forall x y, 1+x==1+y -> x==y.
 
@@ -1098,12 +1099,12 @@ End AlmostField.
 
 Section Field.
 
- Variable Fth : field_theory R rO rI radd rmul rsub ropp rdiv rinv req.
- Let Rth := Fth.(F_R _ _ _ _ _ _ _ _ _ _).
- Let rI_neq_rO := Fth.(F_1_neq_0 _ _ _ _ _ _ _ _ _ _).
- Let rdiv_def := Fth.(Fdiv_def _ _ _ _ _ _ _ _ _ _).
- Let rinv_l := Fth.(Finv_l _ _ _ _ _ _ _ _ _ _).
- Let AFth := F2AF _ _ _ _ _ _ _ _ _ _ Rsth Reqe Fth.
+ Variable Fth : field_theory rO rI radd rmul rsub ropp rdiv rinv req.
+ Let Rth := Fth.(F_R).
+ Let rI_neq_rO := Fth.(F_1_neq_0).
+ Let rdiv_def := Fth.(Fdiv_def).
+ Let rinv_l := Fth.(Finv_l).
+ Let AFth := F2AF Rsth Reqe Fth.
  Let ARth := Rth_ARth Rsth Reqe Rth.
 
 Lemma ring_S_inj : forall x y, 1+x==1+y -> x==y.
diff --git a/contrib/setoid_ring/RealField.v b/contrib/setoid_ring/RealField.v
index 256354d78..194c396ea 100644
--- a/contrib/setoid_ring/RealField.v
+++ b/contrib/setoid_ring/RealField.v
@@ -1,5 +1,5 @@
 Require Import Raxioms.
-Require Export Rdefinitions.
+Require Import Rdefinitions.
 Require Import Ring Field.
 
 Open Local Scope R_scope.
@@ -22,8 +22,7 @@ constructor.
  exact Rplus_opp_r.
 Qed.
 
-Lemma Rfield :
-  field_theory R 0 1 Rplus Rmult Rminus Ropp Rdiv Rinv (eq(A:=R)).
+Lemma Rfield : field_theory 0 1 Rplus Rmult Rminus Ropp Rdiv Rinv (eq(A:=R)).
 Proof.
 constructor.
  exact RTheory.
@@ -101,6 +100,6 @@ Lemma Zeq_bool_complete : forall x y,
   InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp x =
   InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp y ->
   Zeq_bool x y = true.
-Proof gen_phiZ_complete _ _ _ _ _ _ _ _ _ _ Rset Rext Rfield Rgen_phiPOS_not_0.
+Proof gen_phiZ_complete Rset Rext Rfield Rgen_phiPOS_not_0.
 
 Add Field RField : Rfield (infinite Zeq_bool_complete).