diff options
author | 2016-03-18 15:16:24 +0100 | |
---|---|---|
committer | 2016-03-18 15:19:00 +0100 | |
commit | 16939df43a089ac30fec0fcf30a2f648d007cb60 (patch) | |
tree | 98046b9b2f7671d27ac8e69702afa6b0e2a457ef /test-suite/success | |
parent | b4b98349d03c31227d0d86a6e3acda8c3cd5212c (diff) | |
parent | 34c467a4e41e20a9bf1318d47fbc09da94c5ad97 (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/primitiveproj.v | 16 | ||||
-rw-r--r-- | test-suite/success/univers.v | 17 |
2 files changed, 18 insertions, 15 deletions
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 281d707cb..b5e6ccd61 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -35,10 +35,6 @@ Set Implicit Arguments. Check nat. -(* Inductive X (U:Type) := Foo (k : nat) (x : X U). *) -(* Parameter x : X nat. *) -(* Check x.(k). *) - Inductive X (U:Type) := { k : nat; a: k = k -> X U; b : let x := a eq_refl in X U }. Parameter x:X nat. @@ -49,18 +45,8 @@ Inductive Y := { next : option Y }. Check _.(next) : option Y. Lemma eta_ind (y : Y) : y = Build_Y y.(next). -Proof. reflexivity. Defined. - -Variable t : Y. - -Fixpoint yn (n : nat) (y : Y) : Y := - match n with - | 0 => t - | S n => {| next := Some (yn n y) |} - end. +Proof. Fail reflexivity. Abort. -Lemma eta_ind' (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}. -Proof. reflexivity. Defined. (* diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index e00701fb6..269359ae6 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -60,3 +60,20 @@ Qed. (* Submitted by Danko Ilik (bug report #1507); related to LetIn *) Record U : Type := { A:=Type; a:A }. + +(** Check assignement of sorts to inductives and records. *) + +Variable sh : list nat. + +Definition is_box_in_shape (b :nat * nat) := True. +Definition myType := Type. + +Module Ind. +Inductive box_in : myType := + myBox (coord : nat * nat) (_ : is_box_in_shape coord) : box_in. +End Ind. + +Module Rec. +Record box_in : myType := + BoxIn { coord :> nat * nat; _ : is_box_in_shape coord }. +End Rec.
\ No newline at end of file |