From 850f6247e30d44b17fcb63048668619e1a18d7fd Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sat, 16 Nov 2013 21:04:11 +0000
Subject: Slightly faster version of merging substitutions in TacticMatching.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17094 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacticMatching.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/tactics/tacticMatching.ml b/tactics/tacticMatching.ml
index 8d9503318b..26460abbb2 100644
--- a/tactics/tacticMatching.ml
+++ b/tactics/tacticMatching.ml
@@ -54,11 +54,7 @@ let id_map_try_add_name id x m =
     the binding of the right-hand argument shadows that of the left-hand
     argument. *)
 let id_map_right_biased_union m1 m2 =
-    Names.Id.Map.merge begin fun _ x1 x2 ->
-      match x1 , x2 with
-      | _ , Some x | Some x , None -> Some x
-      | _ , _ -> None
-    end m1 m2
+  Names.Id.Map.fold Names.Id.Map.add m2 m1
 
 (** Tests whether the substitution [s] is empty. *)
 let is_empty_subst (ln,lm) =
-- 
cgit v1.2.3