diff options
| author | msozeau | 2009-06-01 18:45:08 +0000 |
|---|---|---|
| committer | msozeau | 2009-06-01 18:45:08 +0000 |
| commit | 837bc87ebb180e47e52bef68925568b250dc60ee (patch) | |
| tree | 290409370fa142c51cd6cae26dafc3503cc8c438 /library | |
| parent | 2089e310ab00d7cc662c1698a4c35f14e750e9fe (diff) | |
Prevent automatic inference of implicit arguments when the auto flag is
not set.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12155 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/impargs.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index b4b61461f4..96c5c2a5c4 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -308,9 +308,9 @@ let const v _ = v let compute_implicits_auto env f manual t = match manual with | [] -> - let l = compute_implicits_flags env f false t in - if not f.auto then List.map (const None) l - else prepare_implicits f l + if not f.auto then [] + else let l = compute_implicits_flags env f false t in + prepare_implicits f l | _ -> compute_manual_implicits env f t f.auto manual let compute_implicits env t = compute_implicits_auto env !implicit_args [] t |