diff options
| author | Erik Martin-Dorel | 2019-11-01 00:49:55 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-11-01 04:43:12 +0100 |
| commit | a37b6f81a3d3922dc89a179b50494d0bbd7afbf6 (patch) | |
| tree | 6ebd1824adab4f45725fcd0953996581f2f7600e /plugins/ssr/ssrclasses.v | |
| parent | 1090b272772c70a79fb082713451a935737cb1d3 (diff) | |
[ssr] Refactor/Extend of under to support more relations
(namely, [RewriteRelation]s beyond Equivalence ones)
Thanks to @CohenCyril for suggesting this enhancement
Diffstat (limited to 'plugins/ssr/ssrclasses.v')
| -rw-r--r-- | plugins/ssr/ssrclasses.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/plugins/ssr/ssrclasses.v b/plugins/ssr/ssrclasses.v index 29486ff4cf..0ae3f8c6a5 100644 --- a/plugins/ssr/ssrclasses.v +++ b/plugins/ssr/ssrclasses.v @@ -12,6 +12,9 @@ (** Compatibility layer for [under] and [setoid_rewrite]. + Note: this file does not require [ssreflect]; it is both required by + [ssrsetoid] and required by [ssrunder]. + Redefine [Coq.Classes.RelationClasses.Reflexive] here, so that doing [Require Import ssreflect] does not [Require Import RelationClasses], and conversely. **) |