diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-14 15:35:27 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-14 15:35:27 +0000 |
| commit | 0388978edc246a64a35c4a0af05d104e3cab03f6 (patch) | |
| tree | 9e9b97084360f8251111730dfee9582e5427c8e2 /interp | |
| parent | a7960723068e47972b2a4b243bd28455c78da7ca (diff) | |
Gestion affinee des implicites
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4637 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index b05151343..10d2a9513 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -485,7 +485,10 @@ let explicit_code imp q = if !Options.v7 & not (Options.do_translate()) then ExplByPos q else ExplByName (name_of_implicit imp) -let is_not_hole = function CHole _ -> false | _ -> true +let is_hole = function CHole _ -> true | _ -> false + +let is_middle_hole a args = + is_hole a && not (List.for_all is_hole args) (* Implicit args indexes are in ascending order *) (* inctx is useful only if there is a last argument to be deduced from ctxt *) @@ -496,7 +499,7 @@ let explicitize loc inctx impl (cf,f) args = let tail = exprec (q+1) (args,impl) in let visible = (!print_implicits & !print_implicits_explicit_args) or - (is_not_hole a & + (not (is_middle_hole a args) & (not (is_inferable_implicit inctx n imp) or (Options.do_translate() & not (stdlib cf)))) in |