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/sphinx/proof-engine/ssreflect-proof-language.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'doc/sphinx/proof-engine') diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 0af23354cc..3db771b0ba 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3756,9 +3756,9 @@ involves the following steps: the corresponding intro pattern :n:`@i_pattern__i` in each goal. 4. Then :tacn:`under` checks that the first n subgoals - are (quantified) Leibniz equalities or registered Setoid equalities - between a term and an evar (e.g. ``m - m = ?F2 m`` in the running - example). + are (quantified) Leibniz equalities, double implications or + registered Setoid equalities between a term and an evar + (e.g. ``m - m = ?F2 m`` in the running example). 5. If so :tacn:`under` protects these n goals against an accidental instantiation of the evar. -- cgit v1.2.3