Merge PR #11132: Fixing bugs in the computation of implicit arguments for `Fixpoint` with a let binder

Reviewed-by: Zimmi48
Reviewed-by: ejgallego

1 files changed, 5 insertions, 1 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 77a2c1c8e6..8b457ab37b 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