diff options
author | 2015-01-25 14:42:51 +0100 | |
---|---|---|
committer | 2015-01-25 14:42:51 +0100 | |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/bugs/closed/shouldsucceed/2733.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2733.v')
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2733.v | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2733.v b/test-suite/bugs/closed/shouldsucceed/2733.v deleted file mode 100644 index fd7bd3bd..00000000 --- a/test-suite/bugs/closed/shouldsucceed/2733.v +++ /dev/null @@ -1,26 +0,0 @@ -Definition goodid : forall {A} (x: A), A := fun A x => x. -Definition wrongid : forall A (x: A), A := fun {A} x => x. - -Inductive ty := N | B. - -Inductive alt_list : ty -> ty -> Type := - | nil {k} : alt_list k k - | Ncons {k} : nat -> alt_list B k -> alt_list N k - | Bcons {k} : bool -> alt_list N k -> alt_list B k. - -Definition trullynul k {k'} (l : alt_list k k') := -match k,l with - |N,l' => Ncons 0 (Bcons true l') - |B,l' => Bcons true (Ncons 0 l') -end. - -Fixpoint app (P : forall {k k'}, alt_list k k' -> alt_list k k') {t1 t2} (l : alt_list t1 t2) {struct l}: forall {t3}, alt_list t2 t3 -> -alt_list t1 t3 := - match l with - | nil _ => fun _ l2 => P l2 - | Ncons _ n l1 => fun _ l2 => Ncons n (app (@P) l1 l2) - | Bcons _ b l1 => fun _ l2 => Bcons b (app (@P) l1 l2) - end. - -Check (fun {t t'} (l: alt_list t t') => - app trullynul (goodid l) (wrongid _ nil)). |