diff options
| author | herbelin | 2003-10-15 13:38:24 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-15 13:38:24 +0000 |
| commit | 2104447c823a67bb5fea36957bfec5f271394bf2 (patch) | |
| tree | 5679558b09830afbe6e7e425dc985755643211c7 /interp/constrextern.ml | |
| parent | 3cc0d63f5951e4053652baa51ed26e2494c7d1fa (diff) | |
Gestion encore plus affinee des implicites
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4641 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 10d2a9513d..ea17a9fba5 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -476,8 +476,7 @@ let stdlib = function | Some r -> let dir,id = repr_path (sp_of_global r) in (is_coq_root (Lib.library_dp()) or is_coq_root dir) - && not (List.mem (string_of_id id) - ["Zlength";"Zlength_correct";"eq_ind"]) + && not (List.mem (string_of_id id) ["Zlength"]) | None -> false let explicit_code imp q = @@ -487,8 +486,8 @@ let explicit_code imp q = let is_hole = function CHole _ -> true | _ -> false -let is_middle_hole a args = - is_hole a && not (List.for_all is_hole args) +let is_significant_implicit a impl tail = + not (is_hole a) or (tail = [] & not (List.for_all is_status_implicit impl)) (* Implicit args indexes are in ascending order *) (* inctx is useful only if there is a last argument to be deduced from ctxt *) @@ -499,7 +498,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 - (not (is_middle_hole a args) & + (is_significant_implicit a impl tail & (not (is_inferable_implicit inctx n imp) or (Options.do_translate() & not (stdlib cf)))) in @@ -531,7 +530,7 @@ let rec skip_coercion dest_ref (f,args as app) = (match Classops.hide_coercion r with | Some n -> if n >= List.length args then app - else (* We skip a coercion *) + else (* We skip a coercion *) let fargs = list_skipn n args in skip_coercion dest_ref (List.hd fargs,List.tl fargs) | None -> app) |