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 | |
| 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
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2733.v | 6 | ||||
| -rw-r--r-- | toplevel/command.ml | 6 |
2 files changed, 10 insertions, 2 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)). diff --git a/toplevel/command.ml b/toplevel/command.ml index 9deaa270f5..5aef9ec66d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -85,7 +85,11 @@ let interp_definition bl red_option c ctypopt = let c, imps2 = interp_casted_constr_evars_impls ~impls ~evdref ~fail_evar:false env_bl c ty in let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in - imps1@(Impargs.lift_implicits nb_args imps2), + (* Check that all implicit arguments inferable from the term is inferable from the type *) + if not (try List.for_all (fun (key,va) -> List.assoc key impsty = va) imps2 with Not_found -> false) + then warn (str "Implicit arguments declaration relies on type." ++ + spc () ++ str "The term declares more implicits than the type here."); + imps1@(Impargs.lift_implicits nb_args impsty), { const_entry_body = body; const_entry_secctx = None; const_entry_type = Some typ; |