From 6b95cbe287b9a4a3b5878f091adefd8f9929a250 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jean-Christophe=20Filli=C3=A2tre?= <filliatr@lri.fr>
Date: Tue, 9 Feb 2010 08:31:40 +0000
Subject: [PATCH] headers
---
Makefile.in | 25 ++++++-------------------
configure.in | 17 +++--------------
misc/headache_config.txt | 12 ++++++++++++
misc/header.txt | 13 +++++++++++++
src/hashcons.ml | 3 ++-
src/hashcons.mli | 3 ++-
src/main.ml | 16 ++++++++++++++++
src/misc.ml | 16 ++++++++++++++++
src/name.ml | 16 ++++++++++++++++
src/name.mli | 16 ++++++++++++++++
src/term.ml | 15 +++++++++++++++
src/term.mli | 15 +++++++++++++++
src/ty.ml | 16 ++++++++++++++++
src/ty.mli | 16 ++++++++++++++++
src/typing.ml | 16 ++++++++++++++++
15 files changed, 180 insertions(+), 35 deletions(-)
create mode 100644 misc/headache_config.txt
create mode 100644 misc/header.txt
diff --git a/Makefile.in b/Makefile.in
index ae2bd27b1e..b24beaf55c 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -1,22 +1,11 @@
##########################################################################
# #
-# The Why platform for program certification #
-# Copyright (C) 2002-2008 #
-# Romain BARDOU #
-# Jean-Fran�ois COUCHOT #
-# Mehdi DOGGUY #
-# Jean-Christophe FILLI�TRE #
-# Thierry HUBERT #
-# Claude MARCH� #
-# Yannick MOY #
-# Christine PAULIN #
-# Yann R�GIS-GIANAS #
-# Nicolas ROUSSET #
-# Xavier URBAIN #
+# Copyright (C) Francois Bobot, Jean-Christophe Filliatre, #
+# Johannes Kanig and Andrei Paskevich. #
# #
# This software is free software; you can redistribute it and/or #
# modify it under the terms of the GNU Library General Public #
-# License version 2, with the special exception on linking #
+# License version 2.1, with the special exception on linking #
# described in file LICENSE. #
# #
# This software is distributed in the hope that it will be useful, #
@@ -1136,11 +1125,9 @@ binary: $(ALLBINARYFILES)
# file headers
##############
headers:
- headache -c doc/headache_config.txt -h doc/header.txt \
- Makefile.in configure.in README \
- */*.ml */*.ml[ily4] tools/*.c bench/c/good/*.c \
- bench/java/good/*.java \
- doc/*.tex
+ headache -c misc/headache_config.txt -h misc/header.txt \
+ Makefile.in configure.in \
+ */*.ml */*.ml[ily4]
# myself
########
diff --git a/configure.in b/configure.in
index b2bb0d796a..77fd1ddafe 100644
--- a/configure.in
+++ b/configure.in
@@ -1,22 +1,11 @@
##########################################################################
# #
-# The Why platform for program certification #
-# Copyright (C) 2002-2008 #
-# Romain BARDOU #
-# Jean-Fran�ois COUCHOT #
-# Mehdi DOGGUY #
-# Jean-Christophe FILLI�TRE #
-# Thierry HUBERT #
-# Claude MARCH� #
-# Yannick MOY #
-# Christine PAULIN #
-# Yann R�GIS-GIANAS #
-# Nicolas ROUSSET #
-# Xavier URBAIN #
+# Copyright (C) Francois Bobot, Jean-Christophe Filliatre, #
+# Johannes Kanig and Andrei Paskevich. #
# #
# This software is free software; you can redistribute it and/or #
# modify it under the terms of the GNU Library General Public #
-# License version 2, with the special exception on linking #
+# License version 2.1, with the special exception on linking #
# described in file LICENSE. #
# #
# This software is distributed in the hope that it will be useful, #
diff --git a/misc/headache_config.txt b/misc/headache_config.txt
new file mode 100644
index 0000000000..d9779b763d
--- /dev/null
+++ b/misc/headache_config.txt
@@ -0,0 +1,12 @@
+# Objective Caml source
+| ".*\\.ml[il4]?" -> frame open:"(*" line:"*" close:"*)"
+| ".*\\.ml[il4]?\\.in" -> frame open:"(*" line:"*" close:"*)"
+| ".*\\.mly" -> frame open:"/*" line:"*" close:"*/"
+# C source
+| ".*\\.c" -> frame open:"/*" line:"*" close:"*/"
+# Misc
+| "configure.in" -> frame open:"#" line:"#" close:"#"
+| "Makefile.in" -> frame open:"#" line:"#" close:"#"
+| "Makefile" -> frame open:"#" line:"#" close:"#"
+| "README.*" -> frame open:"*" line:"*" close:"*"
+| "META.in" -> no
diff --git a/misc/header.txt b/misc/header.txt
new file mode 100644
index 0000000000..166ad8c35c
--- /dev/null
+++ b/misc/header.txt
@@ -0,0 +1,13 @@
+
+Copyright (C) Francois Bobot, Jean-Christophe Filliatre,
+Johannes Kanig and Andrei Paskevich.
+
+This software is free software; you can redistribute it and/or
+modify it under the terms of the GNU Library General Public
+License version 2.1, with the special exception on linking
+described in file LICENSE.
+
+This software is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
+
diff --git a/src/hashcons.ml b/src/hashcons.ml
index addd8794cc..28caac7be3 100644
--- a/src/hashcons.ml
+++ b/src/hashcons.ml
@@ -1,6 +1,7 @@
(**************************************************************************)
(* *)
-(* Copyright (C) Jean-Christophe Filliatre *)
+(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
+(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
diff --git a/src/hashcons.mli b/src/hashcons.mli
index badb96eb95..169be69992 100644
--- a/src/hashcons.mli
+++ b/src/hashcons.mli
@@ -1,6 +1,7 @@
(**************************************************************************)
(* *)
-(* Copyright (C) Jean-Christophe Filliatre *)
+(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
+(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
diff --git a/src/main.ml b/src/main.ml
index 3967ac92ee..670f64fe97 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
+(* Johannes Kanig and Andrei Paskevich. *)
+(* *)
+(* This software is free software; you can redistribute it and/or *)
+(* modify it under the terms of the GNU Library General Public *)
+(* License version 2.1, with the special exception on linking *)
+(* described in file LICENSE. *)
+(* *)
+(* This software is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
+(* *)
+(**************************************************************************)
+
open Term
open Typing
diff --git a/src/misc.ml b/src/misc.ml
index 7eb16ba34b..806433900d 100644
--- a/src/misc.ml
+++ b/src/misc.ml
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
+(* Johannes Kanig and Andrei Paskevich. *)
+(* *)
+(* This software is free software; you can redistribute it and/or *)
+(* modify it under the terms of the GNU Library General Public *)
+(* License version 2.1, with the special exception on linking *)
+(* described in file LICENSE. *)
+(* *)
+(* This software is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
+(* *)
+(**************************************************************************)
+
let combine n acc =
let r = acc * 65599 + n in
if r < 0 then
diff --git a/src/name.ml b/src/name.ml
index 5d5f7434c3..8266800ea2 100644
--- a/src/name.ml
+++ b/src/name.ml
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
+(* Johannes Kanig and Andrei Paskevich. *)
+(* *)
+(* This software is free software; you can redistribute it and/or *)
+(* modify it under the terms of the GNU Library General Public *)
+(* License version 2.1, with the special exception on linking *)
+(* described in file LICENSE. *)
+(* *)
+(* This software is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
+(* *)
+(**************************************************************************)
+
type t = { tag : int ; name : string }
let fresh =
diff --git a/src/name.mli b/src/name.mli
index 6ef7ffb020..c76c0a4fab 100644
--- a/src/name.mli
+++ b/src/name.mli
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
+(* Johannes Kanig and Andrei Paskevich. *)
+(* *)
+(* This software is free software; you can redistribute it and/or *)
+(* modify it under the terms of the GNU Library General Public *)
+(* License version 2.1, with the special exception on linking *)
+(* described in file LICENSE. *)
+(* *)
+(* This software is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
+(* *)
+(**************************************************************************)
+
type t
(** the type of Names *)
diff --git a/src/term.ml b/src/term.ml
index 8190cfc06b..1e120214f7 100644
--- a/src/term.ml
+++ b/src/term.ml
@@ -1,3 +1,18 @@
+(**************************************************************************)
+(* *)
+(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
+(* Johannes Kanig and Andrei Paskevich. *)
+(* *)
+(* This software is free software; you can redistribute it and/or *)
+(* modify it under the terms of the GNU Library General Public *)
+(* License version 2.1, with the special exception on linking *)
+(* described in file LICENSE. *)
+(* *)
+(* This software is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
+(* *)
+(**************************************************************************)
type label = string
diff --git a/src/term.mli b/src/term.mli
index 6cc1f679a0..98b00d641b 100644
--- a/src/term.mli
+++ b/src/term.mli
@@ -1,3 +1,18 @@
+(**************************************************************************)
+(* *)
+(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
+(* Johannes Kanig and Andrei Paskevich. *)
+(* *)
+(* This software is free software; you can redistribute it and/or *)
+(* modify it under the terms of the GNU Library General Public *)
+(* License version 2.1, with the special exception on linking *)
+(* described in file LICENSE. *)
+(* *)
+(* This software is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
+(* *)
+(**************************************************************************)
type label
diff --git a/src/ty.ml b/src/ty.ml
index 8a07b3bf80..6b2ecb2865 100644
--- a/src/ty.ml
+++ b/src/ty.ml
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
+(* Johannes Kanig and Andrei Paskevich. *)
+(* *)
+(* This software is free software; you can redistribute it and/or *)
+(* modify it under the terms of the GNU Library General Public *)
+(* License version 2.1, with the special exception on linking *)
+(* described in file LICENSE. *)
+(* *)
+(* This software is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
+(* *)
+(**************************************************************************)
+
type node =
| BVar of int
| Var of Name.t
diff --git a/src/ty.mli b/src/ty.mli
index 35bd012085..20955e8385 100644
--- a/src/ty.mli
+++ b/src/ty.mli
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
+(* Johannes Kanig and Andrei Paskevich. *)
+(* *)
+(* This software is free software; you can redistribute it and/or *)
+(* modify it under the terms of the GNU Library General Public *)
+(* License version 2.1, with the special exception on linking *)
+(* described in file LICENSE. *)
+(* *)
+(* This software is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
+(* *)
+(**************************************************************************)
+
type node= private
| BVar of int
| Var of Name.t
diff --git a/src/typing.ml b/src/typing.ml
index 16735d8c71..290e570fcc 100644
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
+(* Johannes Kanig and Andrei Paskevich. *)
+(* *)
+(* This software is free software; you can redistribute it and/or *)
+(* modify it under the terms of the GNU Library General Public *)
+(* License version 2.1, with the special exception on linking *)
+(* described in file LICENSE. *)
+(* *)
+(* This software is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
+(* *)
+(**************************************************************************)
+
open Term
module Env : sig
--
GitLab