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.
---
 doc/stdlib/hidden-files             | 1 +
 doc/stdlib/index-list.html.template | 1 +
 2 files changed, 2 insertions(+)

(limited to 'doc/stdlib')

diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index 46175e37ed..4f8986984f 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -77,3 +77,4 @@ plugins/setoid_ring/Rings_Q.v
 plugins/setoid_ring/Rings_R.v
 plugins/setoid_ring/Rings_Z.v
 plugins/setoid_ring/ZArithRing.v
+plugins/ssr/ssrsetoid.v
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index dcfe4a08f3..2673d8db82 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -602,6 +602,7 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     plugins/ssrmatching/ssrmatching.v
+    plugins/ssr/ssrclasses.v
     plugins/ssr/ssreflect.v
     plugins/ssr/ssrbool.v
     plugins/ssr/ssrfun.v
-- 
cgit v1.2.3


From a37b6f81a3d3922dc89a179b50494d0bbd7afbf6 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 1 Nov 2019 00:49:55 +0100
Subject: [ssr] Refactor/Extend of under to support more relations

(namely, [RewriteRelation]s beyond Equivalence ones)

Thanks to @CohenCyril for suggesting this enhancement
---
 doc/stdlib/hidden-files | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/stdlib')

diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index 4f8986984f..6699252cee 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -77,4 +77,5 @@ plugins/setoid_ring/Rings_Q.v
 plugins/setoid_ring/Rings_R.v
 plugins/setoid_ring/Rings_Z.v
 plugins/setoid_ring/ZArithRing.v
+plugins/ssr/ssrunder.v
 plugins/ssr/ssrsetoid.v
-- 
cgit v1.2.3