diff options
-rw-r--r-- | test-suite/success/coercions.v | 34 |
1 files changed, 32 insertions, 2 deletions
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index d4fa132d1..9389c9d32 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -130,7 +130,7 @@ Local Coercion l2v2 : list >-> vect. of coercions *) Fail Check (fun l : list (T1 * T1) => (l : vect _ _)). Check (fun l : list (T1 * T1) => (l2v2 l : vect _ _)). -Section what_we_could_do. +End what_we_could_do. (** Unit test for Prop as source class *) @@ -155,4 +155,34 @@ Module TestPropAsSourceCoercion. (* Print test. -- reveals [hpure] coercions *) -End TestPropAsSourceCoercion.
\ No newline at end of file +End TestPropAsSourceCoercion. + + +(** Unit test for Type as source class *) + +Module TestTypeAsSourceCoercion. + + Require Import Coq.Setoids.Setoid. + + Record setoid := { A : Type ; R : relation A ; eqv : Equivalence R }. + + Definition default_setoid (T : Type) : setoid + := {| A := T ; R := eq ; eqv := _ |}. + + Coercion default_setoid : Sortclass >-> setoid. + + Definition foo := Type : setoid. + + Inductive type := U | Nat. + Inductive term : type -> Type := + | ty (_ : Type) : term U + | nv (_ : nat) : term Nat. + + Coercion ty : Sortclass >-> term. + + Definition ty1 := Type : term _. + Definition ty2 := Prop : term _. + Definition ty3 := Set : term _. + Definition ty4 := (Type : Type) : term _. + +End TestTypeAsSourceCoercion. |