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

1 files changed, 0 insertions, 13 deletions

diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 226dfbd22..d009a456e 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.SetoidTactics") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -24,18 +23,6 @@ Export ProperNotations.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** Setoid relation on a given support: declares a relation as a setoid
-   for use with rewrite. It helps choosing if a rewrite should be handled
-   by setoid_rewrite or the regular rewrite using leibniz equality.
-   Users can declare an [SetoidRelation A RA] anywhere to declare default 
-   relations. This is also done automatically by the [Declare Relation A RA]
-   commands. *)
-
-Class SetoidRelation A (R : relation A).
-
-Instance impl_setoid_relation : SetoidRelation impl.
-Instance iff_setoid_relation : SetoidRelation iff.
-
 (** Default relation on a given support. Can be used by tactics
    to find a sensible default relation on any carrier. Users can 
    declare an [Instance def : DefaultRelation A RA] anywhere to