From eabcd5cfe9d96192747d40776668489f9c5e545c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 6 May 2019 17:05:13 +0200
Subject: Tentative alternative fix for #9992.

We crawl the context in the other direction, preventing the allocation of
the return boolean and enhancing sharing. This fast-path is assuming the
heuristic that the variable being renamed always appears in the context,
otherwise we would be renaming for nothing. It seems to always be the
case, due to the way we pick the set of names to be avoided.
---
 engine/evarutil.ml | 25 ++++++++++---------------
 1 file changed, 10 insertions(+), 15 deletions(-)

(limited to 'engine')

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 4bff98c0c2..42b9fa4714 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -331,21 +331,16 @@ 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 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
+  let rec replace_var_named_declaration id0 id = function
+  | [] -> []
+  | decl :: nc ->
+    if Id.equal id0 (NamedDecl.get_id decl) then
+      (* Stop here, the variable cannot occur before its definition *)
+      (NamedDecl.set_id id decl) :: nc
+    else
+      let nc = replace_var_named_declaration id0 id nc in
+      let vsubst = [id0 , mkVar id] in
+      map_decl (fun c -> replace_vars vsubst c) decl :: nc
   in
   let extract_if_neq id = function
     | Anonymous -> None
-- 
cgit v1.2.3