diff options
| author | Emilio Jesus Gallego Arias | 2019-11-21 18:57:13 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-11-21 18:57:13 +0100 |
| commit | 98165082581fc0950639cfee21e140cac8e916ad (patch) | |
| tree | 3305dc998bd5465b20b7380bc0f4f6f1e0ac25ad /interp | |
| parent | af98bb689a05ccf420da53ee7befacb7c2202942 (diff) | |
| parent | 7255c262c6cc9b3153acf9d2f694196f4e9c10e6 (diff) | |
Merge PR #11132: Fixing bugs in the computation of implicit arguments for `Fixpoint` with a let binder
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
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 57e2214293..ff115a3e48 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 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 |