Fixpoints are traverse during implicits arguments search to toplevel

registration (& CHANGES update)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13826 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 8 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 428ddd6ab..bc067a2f5 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -294,27 +294,31 @@ let implicit_application env ?(allow_partial=true) f ty =
 	in c, avoid
 
 let implicits_of_glob_constr ?(with_products=true) l =
-  let rec aux i c =
-    let abs loc na bk t b =
-      let rest = aux (succ i) b in
-	if bk = Implicit then
+  let add_impl i na bk l =
+ 	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
+	    (ExplByPos (i, name), (true, true, true)) :: l
+	else l in
+  let rec aux i c =
+    let abs na bk b =
+      add_impl i na bk (aux (succ i) b)
     in
       match c with
       | GProd (loc, na, bk, t, b) ->
-	  if with_products then abs loc na bk t b
+	  if with_products then abs na bk b
 	  else 
 	    (if bk = Implicit then
 	       msg_warning (str "Ignoring implicit status of product binder " ++ 
 			      pr_name na ++ str " and following binders");
 	     [])
-      | GLambda (loc, na, bk, t, b) -> abs loc na bk t b
+      | GLambda (loc, na, bk, t, b) -> abs na bk b
       | GLetIn (loc, na, t, b) -> aux i b
+      | GRec (_, fix_kind, nas, args, tys, bds) ->
+       let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
+       list_fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb)
       | _ -> []
   in aux 1 l