diff options
| author | Hugo Herbelin | 2019-11-17 09:39:50 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-11-19 20:03:53 +0100 |
| commit | a81c2de033b37c22be1ca6794ab32347a9917610 (patch) | |
| tree | 16aed2178d8586322bfa00a95703c3a06c5dc231 /interp | |
| parent | 622b4f3ace40313d8dc17141285da32de80b3183 (diff) | |
Fixing bugs in the computation of implicit arguments for fix with a let binder.
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 6 |
2 files changed, 8 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f2cb4ae5c7..f420637e3f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1872,7 +1872,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* We add the recursive functions to the environment *) let env_rec = List.fold_left_i (fun i en name -> let (_,bli,tyi,_) = idl_temp.(i) in - let fix_args = (List.map (fun (na, bk, _, _) -> build_impls bk na) bli) in + let bli = List.filter (fun (_, _, t, _) -> t = None) bli in + let fix_args = List.map (fun (na, bk, t, _) -> build_impls bk na) bli in push_name_env ntnvars (impls_type_list ~args:fix_args tyi) en (CAst.make @@ Name name)) 0 env lf in let idl = Array.map2 (fun (_,_,_,_,bd) (n,bl,ty,before_impls) -> @@ -1903,6 +1904,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (bl,intern_type env' ty,bl_impls)) dl in let env_rec = List.fold_left_i (fun i en name -> let (bli,tyi,_) = idl_tmp.(i) in + let bli = List.filter (fun (_, _, t, _) -> t = None) bli in let cofix_args = List.map (fun (na, bk, _, _) -> build_impls bk na) bli in push_name_env ntnvars (impls_type_list ~args:cofix_args tyi) en (CAst.make @@ Name name)) 0 env lf in 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 |