From a09f5ba40039c0f367c320986011c2d08b953c5b Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 6 Nov 2013 14:52:19 +0000
Subject: Less partial applications in Vars, as well as better memory
 allocation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17065 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarutil.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 2b28c1a752..3de63c9d40 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -312,9 +312,13 @@ let push_rel_context_to_named_context env typ =
   let inst_vars = List.map mkVar ids in
   let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
   let replace_var_named_declaration id0 id (id',b,t) =
-    let id' = if id_ord id0 id' = 0 then id else id' in
+    let id' = if Id.equal id0 id' then id else id' in
     let vsubst = [id0 , mkVar id] in
-    id', Option.map (replace_vars vsubst) b, replace_vars vsubst t
+    let b = match b with
+    | None -> None
+    | Some c -> Some (replace_vars vsubst c)
+    in
+    id', b, replace_vars vsubst t
   in
   let replace_var_named_context id0 id  env =
     let nc = Environ.named_context env in
-- 
cgit v1.2.3