From c5a4aba58f973898ebc9af5176753c7962bddb3c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 9 Aug 2014 18:24:30 +0200
Subject: Adding a primitive to merge ContextSets which is more efficient when
 one of the argument is smaller than the other one.

---
 kernel/univ.ml  | 5 +++++
 kernel/univ.mli | 5 +++++
 2 files changed, 10 insertions(+)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index d3201bcb9d..942c90aa28 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1876,6 +1876,11 @@ struct
   let union (univs, cst) (univs', cst') =
     LSet.union univs univs', Constraint.union cst cst'
 
+  let append (univs, cst) (univs', cst') =
+    let univs = LSet.fold LSet.add univs univs' in
+    let cst = Constraint.fold Constraint.add cst cst' in
+    (univs, cst)
+
   let diff (univs, cst) (univs', cst') =
     LSet.diff univs univs', Constraint.diff cst cst'
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 3779c055d0..c9b7547f29 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -339,6 +339,11 @@ sig
   val of_set : universe_set -> t
 
   val union : t -> t -> t
+
+  val append : t -> t -> t
+  (** Variant of {!union} which is more efficient when the left argument is
+      much smaller than the right one. *)
+
   val diff : t -> t -> t
   val add_universe : universe_level -> t -> t
   val add_constraints : constraints -> t -> t
-- 
cgit v1.2.3