diff options
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2733.v')
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2733.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2733.v b/test-suite/bugs/closed/shouldsucceed/2733.v index 60c3719349..832de4f913 100644 --- a/test-suite/bugs/closed/shouldsucceed/2733.v +++ b/test-suite/bugs/closed/shouldsucceed/2733.v @@ -1,5 +1,8 @@ Unset Asymmetric Patterns. +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 := @@ -21,4 +24,5 @@ alt_list t1 t3 := | Bcons b l1 => fun _ l2 => Bcons b (app (@P) l1 l2) end. -Check (fun {t t'} (l: alt_list t t') => app trullynul l nil). +Check (fun {t t'} (l: alt_list t t') => + app trullynul (goodid l) (wrongid _ nil)). |