diff options
Diffstat (limited to 'interp/impargs.ml')
| -rw-r--r-- | interp/impargs.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/interp/impargs.ml b/interp/impargs.ml index 7e4c4ef4f7..8aa1e62504 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -237,11 +237,11 @@ let is_rigid env sigma t = is_rigid_head sigma t | _ -> true -let find_displayed_name_in all avoid na (env, b) = +let find_displayed_name_in sigma all avoid na (env, b) = let envnames_b = (env, b) in let flag = RenamingElsewhereFor envnames_b in - if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b - else compute_displayed_name_in Evd.empty flag avoid na b + if all then compute_and_force_displayed_name_in sigma flag avoid na b + else compute_displayed_name_in sigma flag avoid na b let compute_implicits_names_gen all env sigma t = let open Context.Rel.Declaration in @@ -249,7 +249,7 @@ let compute_implicits_names_gen all env sigma t = let t = whd_all env sigma t in match kind sigma t with | Prod (na,a,b) -> - let na',avoid' = find_displayed_name_in all avoid na (names,b) in + let na',avoid' = find_displayed_name_in sigma all avoid na (names,b) in aux (push_rel (LocalAssum (na,a)) env) avoid' (na'::names) b | _ -> List.rev names in aux env Id.Set.empty [] t @@ -538,7 +538,7 @@ let subst_implicits_decl subst (r,imps as o) = let r' = fst (subst_global subst r) in if r==r' then o else (r',imps) let subst_implicits (subst,(req,l)) = - (ImplLocal,List.smartmap (subst_implicits_decl subst) l) + (ImplLocal,List.Smart.map (subst_implicits_decl subst) l) let impls_of_context ctx = let map (decl, impl) = match impl with |