Adding a primitive to merge ContextSets which is more efficient when one

of the argument is smaller than the other one.

1 files changed, 5 insertions, 0 deletions

diff --git a/kernel/univ.mli b/kernel/univ.mli
index 3779c055d..c9b7547f2 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