Faster renaming of shadowed variables in evar instance creation.

Instead of blindly renaming the variables in all the terms in the context,
we only do so for those appearing after the variable being renamed. By
typing, we know that the other ones cannot refer to the variable being
replaced.

Fixes #9992.

1 files changed, 16 insertions, 6 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 7c2ecca89e..4bff98c0c2 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -331,11 +331,21 @@ let push_rel_decl_to_named_context
   let map_decl f d =
     NamedDecl.map_constr f d
   in
-  let replace_var_named_declaration id0 id decl =
-    let id' = NamedDecl.get_id decl in
-    let id' = if Id.equal id0 id' then id else id' in
-    let vsubst = [id0 , mkVar id] in
-    decl |> NamedDecl.set_id id' |> map_decl (replace_vars vsubst)
+  let replace_var_named_declaration id0 id nc =
+    let rec replace = function
+    | [] -> false, []
+    | decl :: nc ->
+      let seen, nc = replace nc in
+      if seen then
+        let vsubst = [id0 , mkVar id] in
+        true, (map_decl (fun c -> replace_vars vsubst c) decl) :: nc
+      else if Id.equal id0 (NamedDecl.get_id decl) then
+        true, (NamedDecl.set_id id decl) :: nc
+      else
+        false, decl :: nc
+    in
+    let (_, nc) = replace nc in
+    nc
   in
   let extract_if_neq id = function
     | Anonymous -> None
@@ -366,7 +376,7 @@ let push_rel_decl_to_named_context
           context. Unless [id] is a section variable. *)
       let subst = update_var id0 id subst in
       let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in
-      let nc = List.map (replace_var_named_declaration id0 id) nc in
+      let nc = replace_var_named_declaration id0 id nc in
       (push_var id0 subst, Id.Set.add id avoid, d :: nc)
   | Some id0 when hypnaming = FailIfConflict ->
        user_err Pp.(Id.print id0 ++ str " is already used.")