diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-02-12 23:16:49 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-02-12 23:17:06 +0100 |
| commit | dd0f375656aee2b5eb74380cc3081ef7d8ebe0a4 (patch) | |
| tree | b4801c2d0387f67b06765838138339e01272e39f /test-suite/bugs/closed/2590.v | |
| parent | 69212fa135879b8df4cf3347a6bee0af769a3ee7 (diff) | |
Add test-suite files for closed bugs.
Diffstat (limited to 'test-suite/bugs/closed/2590.v')
| -rw-r--r-- | test-suite/bugs/closed/2590.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2590.v b/test-suite/bugs/closed/2590.v new file mode 100644 index 000000000..e594e9693 --- /dev/null +++ b/test-suite/bugs/closed/2590.v @@ -0,0 +1,19 @@ +Require Import Relation_Definitions RelationClasses Setoid SetoidClass. + +Section Bug. + + Context {A : Type} (R : relation A). + Hypothesis pre : PreOrder R. + Context `{SA : Setoid A}. + + Goal True. + set (SA' := SA). + assert ( forall SA0 : Setoid A, + @PartialOrder A (@equiv A SA0) (@setoid_equiv A SA0) R pre ). + rename SA into SA0. + intro SA. + admit. + admit. +Qed. +End Bug. + |