diff options
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 6 |
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 |