From 3a3ec7e1f306a49008edf47476ea5fb410233b95 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Tue, 19 Sep 2017 16:56:21 +0200
Subject: Adding headers to segmenttree.{ml,mli}.

---
 lib/segmenttree.ml  | 8 ++++++++
 lib/segmenttree.mli | 8 ++++++++
 2 files changed, 16 insertions(+)

(limited to 'lib')

diff --git a/lib/segmenttree.ml b/lib/segmenttree.ml
index 9ce348a0b..d0ded4cb5 100644
--- a/lib/segmenttree.ml
+++ b/lib/segmenttree.ml
@@ -1,3 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 (** This module is a very simple implementation of "segment trees".
 
     A segment tree of type ['a t] represents a mapping from a union of
diff --git a/lib/segmenttree.mli b/lib/segmenttree.mli
index 3258537b9..e274a6fdc 100644
--- a/lib/segmenttree.mli
+++ b/lib/segmenttree.mli
@@ -1,3 +1,11 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 (** This module is a very simple implementation of "segment trees".
 
     A segment tree of type ['a t] represents a mapping from a union of
-- 
cgit v1.2.3