[ssr] Refactor under's Setoid generalization to ease stdlib2 porting

Changes:
* Add ssrclasses.v that redefines [Reflexive] and [iff_Reflexive];
* Add ssrsetoid.v that links
  [ssrclasses.Reflexive] and [RelationClasses.Reflexive];
* Add [Require Coq.ssr.ssrsetoid] in Setoid.v;
* Update ssrfwd.ml accordingly, using a helper file ssrclasses.ml that
  ports some non-exported material from rewrite.ml;
* Some upside in passing: ssrfwd.ml no more depends on Ltac_plugin;
* Update doc and tests as well.

Summary:
* We can now use the under tactic in two flavors:
 - with the [eq] or [iff] relations: [Require Import ssreflect.]
 - or a [RewriteRelation]: [Require Import ssreflect. Require Setoid.]
   (while [ssreflect] does not require [RelationClasses] nor [Setoid],
   and conversely [Setoid] does not require [ssreflect]).
* The file ssrsetoid.v could be skipped when porting under to stdlib2.

1 files changed, 2 insertions, 0 deletions

diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 2f8be5de12..ddc9967bfa 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -12,6 +12,8 @@ Require Export Coq.Classes.SetoidTactics.
 
 Export Morphisms.ProperNotations.
 
+Require Coq.ssr.ssrsetoid.
+
 (** For backward compatibility *)
 
 Definition Setoid_Theory := @Equivalence.