From 895d34a264d9d90adfe4f0618c3bb0663dc01615 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 5 Dec 2015 12:53:20 +0100
Subject: Leveraging GADTs to provide a better Dyn API.

---
 lib/util.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib/util.mli')

diff --git a/lib/util.mli b/lib/util.mli
index 1dc405fcbe..0ce6cc6603 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -111,5 +111,7 @@ val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
 type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
 (** Used for browsable-until structures. *)
 
+type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq
+
 val open_utf8_file_in : string -> in_channel
 (** Open an utf-8 encoded file and skip the byte-order mark if any. *)
-- 
cgit v1.2.3


From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 20 Jan 2016 17:25:10 +0100
Subject: Update copyright headers.

---
 lib/util.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib/util.mli')

diff --git a/lib/util.mli b/lib/util.mli
index 1dc405fcbe..4156af6728 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
-- 
cgit v1.2.3


From 06fa0334047a9400d0b5a144601fca35746a53b8 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 17 Feb 2016 10:32:40 +0100
Subject: CLEANUP: Renaming "Util.compose" function to "%"

I propose to change the name of the "Util.compose" function to "%".

Reasons:

1. If one wants to express function composition,
   then the new name enables us to achieve this goal easier.

2. In "Batteries Included" they had made the same choice.
---
 lib/util.mli | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'lib/util.mli')

diff --git a/lib/util.mli b/lib/util.mli
index 7923c65a3b..559874bb83 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -83,7 +83,15 @@ val matrix_transpose : 'a list list -> 'a list list
 (** {6 Functions. } *)
 
 val identity : 'a -> 'a
-val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
+
+(** Function composition: the mathematical [∘] operator.
+
+    So [g % f] is a synonym for [fun x -> g (f x)].
+
+    Also because [%] is right-associative, [h % g % f] means [fun x -> h (g (f x))].
+*)
+val (%) : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
+
 val const : 'a -> 'b -> 'a
 val iterate : ('a -> 'a) -> int -> 'a -> 'a
 val repeat : int -> ('a -> unit) -> 'a -> unit
-- 
cgit v1.2.3


From 0dfd0fb7d7c04eedfb3b161b9b5cfab103c17916 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 13 Mar 2016 17:48:28 +0100
Subject: Adding a few functions on type union.

---
 lib/util.mli | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'lib/util.mli')

diff --git a/lib/util.mli b/lib/util.mli
index 559874bb83..6bed7e3552 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -114,7 +114,15 @@ val iraise : iexn -> 'a
 type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
 (** Union type *)
 
+module Union :
+sig
+  val map : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
+  val equal : ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> ('a, 'b) union -> ('a, 'b) union -> bool
+  val fold_left : ('c -> 'a -> 'c) -> ('c -> 'b -> 'c) -> 'c -> ('a, 'b) union -> 'c
+end
+
 val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
+(** Alias for [Union.map] *)
 
 type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
 (** Used for browsable-until structures. *)
-- 
cgit v1.2.3