Fixing bugs in the computation of implicit arguments for fix with a let binder.

1 files changed, 5 insertions, 1 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 455471a472..4301242fd9 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -219,6 +219,10 @@ let implicits_of_glob_constr ?(with_products=true) l =
     | GLetIn (na, b, t, c) -> aux c
     | GRec (fix_kind, nas, args, tys, bds) ->
       let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
-      List.fold_right (fun (na,bk,t,_) l -> add_impl ?loc:c.CAst.loc na bk l) args.(nb) (aux bds.(nb))
+      List.fold_right (fun (na,bk,t,_) l ->
+          match t with
+          | Some _ -> l
+          | _ -> add_impl ?loc:c.CAst.loc na bk l)
+        args.(nb) (aux bds.(nb))
     | _ -> []
   in aux l