From 23cbf43f353c50fa72b72d694611c5c14367cea2 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 6 Jan 2016 00:58:42 +0100
Subject: Protect code against changes in Map interface.

The Map interface of upcoming OCaml 4.03 includes a new union operator. In
order to make our homemade implementation of Maps compatible with OCaml
versions from 3.12 to 4.03, we define our own signatures for Maps.
---
 lib/cMap.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib/cMap.ml')

diff --git a/lib/cMap.ml b/lib/cMap.ml
index cf590d96c3..048a690812 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -16,7 +16,7 @@ module type S = Map.S
 
 module type ExtS =
 sig
-  include Map.S
+  include CSig.MapS
   module Set : CSig.SetS with type elt = key
   val update : key -> 'a -> 'a t -> 'a t
   val modify : key -> (key -> 'a -> 'a) -> 'a t -> 'a t
-- 
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/cMap.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib/cMap.ml')

diff --git a/lib/cMap.ml b/lib/cMap.ml
index 048a690812..665e1a2163 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -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 e9675e068f9e0e92bab05c030fb4722b146123b8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 3 Feb 2016 16:20:46 +0100
Subject: Adding a "get" primitive to map signature.

It is similar to find but raises an assertion failure instead of a Not_found
when the element is not encountered. Using it will give stronger invariants.
---
 lib/cMap.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib/cMap.ml')

diff --git a/lib/cMap.ml b/lib/cMap.ml
index d1a32b7aa5..4b058380c6 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -25,6 +25,7 @@ module type ExtS =
 sig
   include CSig.MapS
   module Set : CSig.SetS with type elt = key
+  val get : key -> 'a t -> 'a
   val update : key -> 'a -> 'a t -> 'a t
   val modify : key -> (key -> 'a -> 'a) -> 'a t -> 'a t
   val domain : 'a t -> Set.t
@@ -207,4 +208,5 @@ module Make(M : Map.OrderedType) =
 struct
   include Map.Make(M)
   include MapExt(M)
+  let get k m = try find k m with Not_found -> assert false
 end
-- 
cgit v1.2.3