diff options
| author | msozeau | 2010-06-09 18:19:16 +0000 |
|---|---|---|
| committer | msozeau | 2010-06-09 18:19:16 +0000 |
| commit | 2cf5036431304d5a3e6393d5fd5827798ea98983 (patch) | |
| tree | 1ef0caa5a199d7f5dc3703504c7c54a1b07d6bc4 /interp/implicit_quantifiers.ml | |
| 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/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 33 |
1 files changed, 21 insertions, 12 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 89ec5f1f11..cad48a5a1c 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 |