diff options
| author | ppedrot | 2013-11-16 21:04:11 +0000 |
|---|---|---|
| committer | ppedrot | 2013-11-16 21:04:11 +0000 |
| commit | 850f6247e30d44b17fcb63048668619e1a18d7fd (patch) | |
| tree | 0434b9344888da77e83e8386b97b244336c9bdce | |
| parent | f00c94820af4c64cc2391fcc22f38b4fe846a62a (diff) | |
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
| -rw-r--r-- | tactics/tacticMatching.ml | 6 |
1 files changed, 1 insertions, 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) = |