From a81c2de033b37c22be1ca6794ab32347a9917610 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 17 Nov 2019 09:39:50 +0100
Subject: Fixing bugs in the computation of implicit arguments for fix with a
 let binder.

---
 interp/implicit_quantifiers.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'interp/implicit_quantifiers.ml')

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
-- 
cgit v1.2.3