From d60b807c868f4d54a273549519ea51c196242370 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Tue, 6 Aug 2019 22:52:16 +0200
Subject: [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.
---
 plugins/ssr/ssreflect_plugin.mlpack | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ssr/ssreflect_plugin.mlpack')

diff --git a/plugins/ssr/ssreflect_plugin.mlpack b/plugins/ssr/ssreflect_plugin.mlpack
index 824348fee7..66aa6b3e67 100644
--- a/plugins/ssr/ssreflect_plugin.mlpack
+++ b/plugins/ssr/ssreflect_plugin.mlpack
@@ -7,7 +7,7 @@ Ssrview
 Ssrbwd
 Ssrequality
 Ssripats
+Ssrclasses
 Ssrfwd
 Ssrparser
 Ssrvernac
-
-- 
cgit v1.2.3


From 1857d474d06b23df32c16be26225ee174ad4d6c1 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 1 Nov 2019 01:45:33 +0100
Subject: [ssr] chore: Remove ssrclasses.{ml,mli} (now unneeded)

---
 plugins/ssr/ssreflect_plugin.mlpack | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/ssr/ssreflect_plugin.mlpack')

diff --git a/plugins/ssr/ssreflect_plugin.mlpack b/plugins/ssr/ssreflect_plugin.mlpack
index 66aa6b3e67..46669998b9 100644
--- a/plugins/ssr/ssreflect_plugin.mlpack
+++ b/plugins/ssr/ssreflect_plugin.mlpack
@@ -7,7 +7,6 @@ Ssrview
 Ssrbwd
 Ssrequality
 Ssripats
-Ssrclasses
 Ssrfwd
 Ssrparser
 Ssrvernac
-- 
cgit v1.2.3