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

2 files changed, 13 insertions, 13 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1634.v b/test-suite/bugs/closed/shouldsucceed/1634.v
index 9e50f6f25..205e82798 100644
--- a/test-suite/bugs/closed/shouldsucceed/1634.v
+++ b/test-suite/bugs/closed/shouldsucceed/1634.v
@@ -3,22 +3,22 @@ Require Export Setoid.
 
 Variable A : Type.
 Variable S : A -> Type.
-Variable Seq : forall (a:A), relation (S a).
+Variable Seq : forall {a:A}, relation (S a).
 
-Hypothesis Seq_refl : forall (a:A) (x : S a), Seq a x x.
-Hypothesis Seq_sym : forall (a:A) (x y : S a), Seq a x y -> Seq a y x.
-Hypothesis Seq_trans : forall (a:A) (x y z : S a), Seq a x y -> Seq a y z ->
-Seq
-a x z.
+Hypothesis Seq_refl : forall {a:A} (x : S a), Seq x x.
+Hypothesis Seq_sym : forall {a:A} (x y : S a), Seq x y -> Seq y x.
+Hypothesis Seq_trans : forall {a:A} (x y z : S a), Seq x y -> Seq y z ->
+Seq x z.
 
-Add Relation S Seq
+Add Relation (S a) Seq
  reflexivity proved by Seq_refl
  symmetry proved by Seq_sym
  transitivity proved by Seq_trans
  as S_Setoid.
 
-Goal forall (a : A) (x y : S a), Seq a x y -> Seq a x y.
+Goal forall (a : A) (x y : S a), Seq x y -> Seq x y.
   intros a x y H.
-  setoid_replace x with y using relation Seq.
-  apply Seq_refl. trivial.
+  setoid_replace x with y. 
+  reflexivity.
+  trivial.
 Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v
index a963b225f..95bbab92a 100644
--- a/test-suite/bugs/closed/shouldsucceed/846.v
+++ b/test-suite/bugs/closed/shouldsucceed/846.v
@@ -138,15 +138,15 @@ Proof.
   right; assumption.
   intros l _ r.
   apply (step (A:=L' A l)).
-  exact (inl _ (inl _ r)).
+  exact (inl (inl r)).
   intros l _ r1 _ r2.
   apply (step (A:=L' A l)).
   (* unfold L' in * |- *.
   Check 0. *)
-  exact (inl _ (inr _ (pair r1 r2))).
+  exact (inl (inr (pair r1 r2))).
   intros l _ r.
   apply  (step (A:=L' A l)).
-  exact (inr _ r).
+  exact (inr r).
 Defined.
 
 Definition L'inG: forall A: Set, L' A (true::nil) -> G A.