Remove spurious .d, better tactics.

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

3 files changed, 26 insertions, 13 deletions

diff --git a/theories/Classes/Init.v.d b/theories/Classes/Init.v.d
deleted file mode 100644
index 482ac0796e..0000000000
--- a/theories/Classes/Init.v.d
+++ /dev/null
@@ -1 +0,0 @@
-theories/Classes/Init.vo theories/Classes/Init.glob: theories/Classes/Init.v
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 7963a307b7..feafd2b3c2 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -89,6 +89,7 @@ Ltac trans y := do_setoid_trans y.
 Ltac setoid_refl :=
   match goal with
     | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X)
+    | [ H : ?X =!= ?X |- _ ] => elim H ; setoid_refl
     | [ |- ?R ?X _ ] => apply (equiv_refl (R:=R) X)
     | [ |- ?R ?A ?X _ ] => apply (equiv_refl (R:=R A) X)
     | [ |- ?R ?A ?B ?X _ ] => apply (equiv_refl (R:=R A B) X)
@@ -128,22 +129,31 @@ Qed.
 
 Open Scope type_scope.
 
+(** Need to fix fresh to not fail if some arguments are not identifiers. *)
+(* Ltac setoid_sat ::= *)
+(*   match goal with *)
+(*     | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" y x in add_hypothesis name (equiv_sym H) *)
+(*     | [ H : ?x =!= ?y |- _ ] => let name:=fresh "Hneq" y x in add_hypothesis name (nequiv_sym H) *)
+(*     | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" x z in add_hypothesis name (equiv_trans H H') *)
+(*     | [ H : ?x == ?y, H' : ?y =!= ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (equiv_nequiv H H') *)
+(*     | [ H : ?x =!= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (nequiv_equiv H H') *)
+(*   end. *)
+
 Ltac setoid_sat :=
-  let add H t := let name := fresh H in add_hypothesis name t in
-    match goal with
-      | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" y x in add name (equiv_sym H)
-      | [ H : ?x =!= ?y |- _ ] => let name:=fresh "Hneq" y x in add name (nequiv_sym H)
-      | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" x z in add name (equiv_trans H H')
-      | [ H : ?x == ?y, H' : ?y =!= ?z |- _ ] => let name:=fresh "Hneq" x z in add name (equiv_nequiv H H')
-      | [ H : ?x =!= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" x z in add name (nequiv_equiv H H')
-    end.
+  match goal with
+    | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_sym H)
+    | [ H : ?x =!= ?y |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_sym H)
+    | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_trans H H')
+    | [ H : ?x == ?y, H' : ?y =!= ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (equiv_nequiv H H')
+    | [ H : ?x =!= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_equiv H H')
+  end.
 
 Ltac setoid_saturate := repeat setoid_sat.
 
 Ltac setoidify_tac :=
   match goal with
     | [ s : Setoid ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
-    | [ s : Setoid ?A ?R |- ?R ?x ?y ] => change R with (@equiv A R s)
+    | [ s : Setoid ?A ?R |- ?R ?x ?y ] => change (R x y) with (@equiv A R s x y)
   end.
 
 Ltac setoidify := repeat setoidify_tac.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index aa151772d4..cd96269f8f 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -20,13 +20,13 @@ Unset Strict Implicit.
 Require Import Coq.Classes.SetoidClass.
 
 Class [ Setoid A R ] => EqDec :=
-  equiv_dec : forall x y : A, { R x y } + { ~ R x y }.
+  equiv_dec : forall x y : A, { x == y } + { x =!= y }.
 
 Infix "==" := equiv_dec (no associativity, at level 70).
 
 Require Import Coq.Program.Program.
 
-Program Definition nequiv_dec [ EqDec A R ] (x y : A) : { ~ R x y } + { R x y } :=
+Program Definition nequiv_dec [ EqDec A R ] (x y : A) : { x =!= y } + { x == y } :=
   if x == y then right else left.
 
 Infix "<>" := nequiv_dec (no associativity, at level 70).
@@ -72,7 +72,7 @@ Program Instance [ EqDec A eq, EqDec B eq ] => prod_eqdec : EqDec (prod A B) eq
       else right
     else right.
 
-Solve Obligations using program_simpl ; red ; intro ; autoinjections ; discriminates.
+Solve Obligations using unfold equiv ; program_simpl ; try red ; intros ; autoinjections ; discriminates.
 
 Program Instance [ EqDec A eq ] => bool_function_eqdec : EqDec (bool -> A) eq :=
   equiv_dec f g := 
@@ -81,16 +81,20 @@ Program Instance [ EqDec A eq ] => bool_function_eqdec : EqDec (bool -> A) eq :=
       else right
     else right.
 
+Solve Obligations using unfold equiv ; program_simpl.
+
 Require Import Coq.Program.FunctionalExtensionality.
 
 Next Obligation.
 Proof.
+  unfold equiv.
   extensionality x.
   destruct x ; auto.
 Qed.
 
 Next Obligation.
 Proof.
+  unfold equiv in *.
   red ; intro ; subst.
   discriminates.
 Qed.