From dfaf7e1ca5aebfdfbef5f32d235a948335f7fda0 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 3 May 2018 17:44:34 +0200 Subject: Remove some occurrences of Evd.empty We address the easy ones, but they should probably be all removed. --- interp/impargs.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'interp/impargs.ml') diff --git a/interp/impargs.ml b/interp/impargs.ml index 2db67c299..8aa1e6250 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 -- cgit v1.2.3