diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-09 18:19:16 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-09 18:19:16 +0000 |
| commit | 2cf5036431304d5a3e6393d5fd5827798ea98983 (patch) | |
| tree | 1ef0caa5a199d7f5dc3703504c7c54a1b07d6bc4 /interp | |
| parent | 41e36fe75b0859480c523e40361b75a13afcfe69 (diff) | |
Fix bug #2262: bad implicit argument number by avoiding counting
products as implicit if they're part of a term and not a type (issue a
warning instead).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13101 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 5 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 33 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.mli | 2 |
3 files changed, 25 insertions, 15 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ceb0748fe..152858984 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1425,8 +1425,9 @@ let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true) | None -> ref Evd.empty | Some evdref -> evdref in - let c = intern_gen (kind=IsType) ~impls !evdref env c in - let imps = Implicit_quantifiers.implicits_of_rawterm c in + let istype = kind = IsType in + let c = intern_gen istype ~impls !evdref env c in + let imps = Implicit_quantifiers.implicits_of_rawterm ~with_products:istype c in Default.understand_tcc_evars ~fail_evar evdref env kind c, imps let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true) diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 89ec5f1f1..cad48a5a1 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -295,19 +295,28 @@ let implicit_application env ?(allow_partial=true) f ty = CAppExpl (loc, (None, id), args), avoid in c, avoid -let implicits_of_rawterm l = +let implicits_of_rawterm ?(with_products=true) l = let rec aux i c = - match c with - RProd (loc, na, bk, t, b) | RLambda (loc, na, bk, t, b) -> - let rest = aux (succ i) b in - if bk = Implicit then - let name = - match na with - Name id -> Some id - | Anonymous -> None - in - (ExplByPos (i, name), (true, true, true)) :: rest - else rest + let abs loc na bk t b = + let rest = aux (succ i) b in + if bk = Implicit then + let name = + match na with + | Name id -> Some id + | Anonymous -> None + in + (ExplByPos (i, name), (true, true, true)) :: rest + else rest + in + match c with + | RProd (loc, na, bk, t, b) -> + if with_products then abs loc na bk t b + else + (if bk = Implicit then + msg_warning (str "Ignoring implicit status of product binder " ++ + pr_name na ++ str " and following binders"); + []) + | RLambda (loc, na, bk, t, b) -> abs loc na bk t b | RLetIn (loc, na, t, b) -> aux i b | _ -> [] in aux 1 l diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index ac610fe78..0b2ac3e71 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -42,7 +42,7 @@ val generalizable_vars_of_rawconstr : ?bound:Idset.t -> ?allowed:Idset.t -> val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier -val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool * bool)) list +val implicits_of_rawterm : ?with_products:bool -> Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool * bool)) list val combine_params_freevar : Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) -> |