Fix the bug-ridden code used to choose leibniz or generalized

rewriting (thanks to Georges Gonthier for pointing it out). 
We try to find a declared rewrite relation when the equation does not
look like an equality and otherwise try to reduce it to find a leibniz equality
but don't backtrack on generalized rewriting if this fails. This new
behavior make two fsets scripts fail as they are trying to use an
underlying leibniz equality for a declared rewrite relation, a [red]
fixes it.
Do some renaming from "setoid" to "rewrite".
Fix [is_applied_rewrite_relation]'s bad handling of evars and the
environment.
Fix some [dual] hints in RelationClasses.v and assert that any declared
[Equivalence] can be considered a [RewriteRelation].
Fix minor tex output problem in coqdoc.


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

2 files changed, 2 insertions, 1 deletions

diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index e116067af..e09db9b6e 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -1021,7 +1021,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E).
   case_eq (find k' m'); auto; intros e'; rewrite <- find_mapsto_iff.
   intro; elim (Heq k' e'); auto.
   intros k e a m' m'' _ _ Hadd Heq k'.
-  rewrite Hadd, 2 add_o, Heq; auto.
+  red in Heq. rewrite Hadd, 2 add_o, Heq; auto.
   Qed.
 
   Section Fold_More.
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 37cacbc75..10c7ce4a8 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -703,6 +703,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   intros; intro.
   generalize (mem_1 H0).
   rewrite mem_find.
+  red in H.
   rewrite H.
   rewrite grs.
   intros; discriminate.