diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 18:33:25 +0100 |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /test-suite/success/primitiveproj.v | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
Diffstat (limited to 'test-suite/success/primitiveproj.v')
-rw-r--r-- | test-suite/success/primitiveproj.v | 18 |
1 files changed, 3 insertions, 15 deletions
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 281d707c..2fa77049 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,19 +45,11 @@ 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. +Inductive Fdef := { Fa : nat ; Fb := Fa; Fc : Fdef }. +Fail Scheme Fdef_rec := Induction for Fdef Sort Prop. (* Rules for parsing and printing of primitive projections and their eta expansions. |