From 96ba53fca037456f5c10564e18d5ed6502edc247 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 30 Oct 2013 16:46:14 +0000
Subject: More efficient implementation of [Evd.retract_coercible_metas].

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16957 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evd.ml | 26 +++++++++++++++++---------
 1 file changed, 17 insertions(+), 9 deletions(-)

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 67cf3a32f2..1513166326 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -768,15 +768,23 @@ let meta_merge evd1 evd2 =
 type metabinding = metavariable * constr * instance_status
 
 let retract_coercible_metas evd =
-  let mc,ml =
-    Metamap.fold (fun n v (mc,ml) ->
-      match v with
-	| Clval (na,(b,(Conv,CoerceToType as s)),typ) ->
-	    (n,b.rebus,s)::mc, Metamap.add n (Cltyp (na,typ)) ml
-	| v ->
-	    mc, Metamap.add n v ml)
-      evd.metas ([],Metamap.empty) in
-  mc, { evd with metas = ml }
+  let mc = ref [] in
+  let map n v = match v with
+  | Clval (na, (b, (Conv, CoerceToType as s)), typ) ->
+    let () = mc := (n, b.rebus, s) :: !mc in
+    Cltyp (na, typ)
+  | v -> v
+  in
+  let metas = Metamap.mapi map evd.metas in
+  !mc, {
+    defn_evars = evd.defn_evars;
+    undf_evars = evd.undf_evars;
+    universes  = evd.universes;
+    univ_cstrs = evd.univ_cstrs;
+    conv_pbs = evd.conv_pbs;
+    last_mods = evd.last_mods;
+    metas;
+    effects = evd.effects; }
 
 let subst_defined_metas bl c =
   let rec substrec c = match kind_of_term c with
-- 
cgit v1.2.3