Bug squashing day !

- Closed bugs 121, 1696, 1438, 1425, 1696, 1604, 1738, 1760, 1683 related to
setoids. Add corresponding test files.
- Add new modulo_zeta flag to control zeta during unification (e.g. not
allowed for setoid_rewrite unification, but ok for almost everything
else).
- Various fixes in class_tactics with respect to evars and error
messages.
- Correct error message for NoOccurenceFound, distinguishing between a
rewrite in the goal or an hypothesis.
- Move notations for ==>, --> and ++> to level 90 as suggested by
Russell O'Conor.


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

6 files changed, 125 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/121.v b/test-suite/bugs/closed/shouldsucceed/121.v
new file mode 100644
index 000000000..d193aa73f
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/121.v
@@ -0,0 +1,17 @@
+Require Import Setoid.
+
+Section Setoid_Bug.
+
+Variable X:Type -> Type.
+Variable Xeq : forall A, (X A) -> (X A) -> Prop.
+Hypothesis Xst : forall A, Equivalence (X A) (Xeq A).
+
+Variable map : forall A B, (A -> B) -> X A -> X B.
+
+Implicit Arguments map [A B].
+
+Goal forall A B (a b:X (B -> A)) (c:X A) (f:A -> B -> A), Xeq _ a b -> Xeq _ b (map f c) -> Xeq _ a (map f c).
+intros A B a b c f Hab Hbc.
+rewrite Hab.
+assumption.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1425.v b/test-suite/bugs/closed/shouldsucceed/1425.v
new file mode 100644
index 000000000..f5fbb8a2a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1425.v
@@ -0,0 +1,13 @@
+Require Import Setoid. 
+
+Parameter recursion : forall A : Set, A -> (nat -> A -> A) -> nat -> A.
+
+Axiom recursion_S :
+  forall (A : Set) (EA : relation A) (a : A) (f : nat -> A -> A) (n : nat),
+    EA (recursion A a f (S n)) (f n (recursion A a f n)).
+
+Goal forall n : nat, recursion nat 0 (fun _ _ => 1) (S n) = 1.
+intro n.
+setoid_rewrite recursion_S.
+reflexivity.
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1604.v b/test-suite/bugs/closed/shouldsucceed/1604.v
new file mode 100644
index 000000000..2d0991cb1
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1604.v
@@ -0,0 +1,7 @@
+Require Import Setoid.
+
+Parameter F : nat -> nat.
+Axiom F_id : forall n : nat, n = F n.
+Goal forall n : nat, F n = n.
+intro n. setoid_rewrite F_id at 2. reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1683.v b/test-suite/bugs/closed/shouldsucceed/1683.v
new file mode 100644
index 000000000..1571ee20e
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1683.v
@@ -0,0 +1,42 @@
+Require Import Setoid.
+
+Section SetoidBug.
+
+Variable ms : Type.
+Variable ms_type : ms -> Type.
+Variable ms_eq : forall (A:ms), relation (ms_type A).
+
+Variable CR : ms.
+
+Record Ring : Type :=
+{Ring_type : Type}.
+
+Variable foo : forall (A:Ring), nat -> Ring_type A.
+Variable IR : Ring.
+Variable IRasCR : Ring_type IR -> ms_type CR.
+
+Definition CRasCRing : Ring := Build_Ring (ms_type CR).
+
+Hypothesis ms_refl : forall A x, ms_eq A x x.
+Hypothesis ms_sym : forall A x y, ms_eq A x y -> ms_eq A y x.
+Hypothesis ms_trans : forall A x y z, ms_eq A x y -> ms_eq A y z -> ms_eq A x z.
+
+Add Parametric Relation A : (ms_type A) (ms_eq A)
+  reflexivity proved by (ms_refl A)
+  symmetry proved by (ms_sym A)
+  transitivity proved by (ms_trans A)
+  as ms_Setoid.
+
+Hypothesis foobar : forall n, ms_eq CR (IRasCR (foo IR n)) (foo CRasCRing n).
+
+Goal forall (b:ms_type CR),
+ ms_eq CR (IRasCR (foo IR O)) b -> 
+ ms_eq CR (IRasCR (foo IR O)) b.
+intros b H.
+rewrite foobar.
+rewrite foobar in H.
+assumption.
+Qed.
+
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1696.v b/test-suite/bugs/closed/shouldsucceed/1696.v
new file mode 100644
index 000000000..0826428a3
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1696.v
@@ -0,0 +1,16 @@
+Require Import Setoid.
+
+Inductive mynat := z : mynat | s : mynat -> mynat.
+
+Parameter E : mynat -> mynat -> Prop.
+Axiom E_equiv : equiv mynat E.
+
+Add Relation mynat E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
+as E_rel.
+
+Notation "x == y" := (E x y) (at level 70).
+
+Goal z == s z -> s z == z. intros H. setoid_rewrite H at 2. reflexivity. Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1738.v b/test-suite/bugs/closed/shouldsucceed/1738.v
new file mode 100644
index 000000000..0deed3663
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1738.v
@@ -0,0 +1,30 @@
+Require Import FSets.
+
+Module SomeSetoids (Import M:FSetInterface.S).
+
+Lemma Equal_refl : forall s, s[=]s.
+Proof. red; split; auto. Qed.
+
+Add Relation t Equal 
+ reflexivity proved by Equal_refl 
+ symmetry proved by eq_sym
+ transitivity proved by eq_trans 
+ as EqualSetoid.
+
+Add Morphism Empty with signature Equal ==> iff as Empty_m.
+Proof.
+unfold Equal, Empty; firstorder.
+Qed.
+
+End SomeSetoids.
+
+Module Test (Import M:FSetInterface.S).
+ Module A:=SomeSetoids M.
+ Module B:=SomeSetoids M. (* lots of warning *)
+
+ Lemma Test : forall s s', s[=]s' -> Empty s -> Empty s'.
+ intros.
+ rewrite H in H0.
+ assumption.
+Qed.
+End Test.
\ No newline at end of file