Fix bugs that were reopened due to the change of setoid

implementation. Mostly syntax changes when declaring parametric
relations, but also some declarations were relying on "default"
relations on some carrier. Added a new DefaultRelation type class that
allows to do that, falling back to the last declared Equivalence
relation by default. This will be bound to Add Relation in the next
commit. 

Also, move the "left" and "right" notations in Program.Utils to "in_left" and
"in_right" to avoid clashes with existing scripts.

Minor change to record to allow choosing the name of the argument for
the record in projections to avoid possible incompatibilities.


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

1 files changed, 9 insertions, 7 deletions

diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 8a435b449..86a2bef80 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -50,6 +50,8 @@ Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
 
 Require Import Coq.Program.Program.
 
+Open Local Scope program_scope.
+
 (** Invert the branches. *)
 
 Program Definition nequiv_dec [ ! EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
@@ -87,7 +89,7 @@ Program Instance bool_eqdec : EqDec (@eq_setoid bool) :=
   equiv_dec := bool_dec.
 
 Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
-  equiv_dec x y := left.
+  equiv_dec x y := in_left.
 
   Next Obligation.
   Proof.
@@ -101,9 +103,9 @@ Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] =>
     dest x as (x1, x2) in 
     dest y as (y1, y2) in 
     if x1 == y1 then 
-      if x2 == y2 then left
-      else right
-    else right.
+      if x2 == y2 then in_left
+      else in_right
+    else in_right.
 
   Solve Obligations using unfold complement ; program_simpl.
 
@@ -114,9 +116,9 @@ Require Import Coq.Program.FunctionalExtensionality.
 Program Instance [ EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) :=
   equiv_dec f g := 
     if f true == g true then
-      if f false == g false then left
-      else right
-    else right.
+      if f false == g false then in_left
+      else in_right
+    else in_right.
 
   Solve Obligations using try red ; unfold equiv, complement ; program_simpl.