aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2848.v
blob: 828e3b8c1f8a544aefb747052c56282da2174d31 (plain)
1
2
3
4
5
6
7
8
9
10
Require Import Setoid.

Parameter value' : Type.
Parameter equiv' : value' -> value' -> Prop.
Axiom cheat : forall {A}, A.
Add Parametric Relation : _ equiv'
  reflexivity proved by (Equivalence.equiv_reflexive cheat)
  transitivity proved by (Equivalence.equiv_transitive cheat)
    as apply_equiv'_rel.
Check apply_equiv'_rel : PreOrder equiv'.