diff options
author | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /library/impargs.ml | |
parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'library/impargs.ml')
-rw-r--r-- | library/impargs.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 3a505ddb..2b2c607c 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: impargs.ml 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: impargs.ml 11576 2008-11-10 19:13:15Z msozeau $ *) open Util open Names @@ -71,6 +71,7 @@ let make_maximal_implicit_args flag = let is_implicit_args () = !implicit_args.main let is_manual_implicit_args () = !implicit_args.manual +let is_auto_implicit_args () = !implicit_args.main && not (is_manual_implicit_args ()) let is_strict_implicit_args () = !implicit_args.strict let is_strongly_strict_implicit_args () = !implicit_args.strongly_strict let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern @@ -577,10 +578,11 @@ type manual_explicitation = Topconstr.explicitation * (bool * bool) let compute_implicits_with_manual env typ enriching l = compute_manual_implicits env !implicit_args typ enriching l -let declare_manual_implicits local ref enriching l = +let declare_manual_implicits local ref ?enriching l = let flags = !implicit_args in let env = Global.env () in let t = Global.type_of_global ref in + let enriching = Option.default (is_auto_implicit_args ()) enriching in let l' = compute_manual_implicits env flags t enriching l in let req = if local or isVarRef ref then ImplLocal @@ -588,9 +590,9 @@ let declare_manual_implicits local ref enriching l = in add_anonymous_leaf (inImplicits (req,[ref,l'])) -let maybe_declare_manual_implicits local ref enriching l = +let maybe_declare_manual_implicits local ref ?enriching l = if l = [] then () - else declare_manual_implicits local ref enriching l + else declare_manual_implicits local ref ?enriching l let lift_implicits n = List.map (fun x -> |