diff options
| author | pboutill | 2012-04-27 16:43:24 +0000 |
|---|---|---|
| committer | pboutill | 2012-04-27 16:43:24 +0000 |
| commit | a1a3e3b84bc7dac2ae1ddae1770adde914732315 (patch) | |
| tree | 479a0bfbf3cc74abd5b8a16087565d4b9db82f5e /test-suite | |
| parent | bbf334b38ae4c57b4d619a8f98acc488077efca4 (diff) | |
Implicit arguments of Definition are taken from the type when given by the user.
There is a warning if the term is more precise.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15252 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -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)). |