summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-01-27 11:19:58 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-01-27 11:19:58 +0000
commit877b4347139b187bb2e5151526ae17307d246a12 (patch)
treee9e61f8de6ff2fe6c786554b64cd29f22562b456 /lib
parente431dcf84d7e1a1106a501d53492b672c9d0b86e (diff)
Ajout license, README, copyright notices
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'lib')
-rw-r--r--lib/Coqlib.v15
-rw-r--r--lib/Floats.v15
-rw-r--r--lib/Inclusion.v12
-rw-r--r--lib/Integers.v15
-rw-r--r--lib/Iteration.v12
-rw-r--r--lib/Lattice.v12
-rw-r--r--lib/Maps.v15
-rw-r--r--lib/Ordered.v12
-rw-r--r--lib/Parmov.v17
9 files changed, 125 insertions, 0 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 7bee366..c14ed79 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -1,3 +1,18 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU General Public License as published by *)
+(* the Free Software Foundation, either version 2 of the License, or *)
+(* (at your option) any later version. This file is also distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
(** This file collects a number of definitions and theorems that are
used throughout the development. It complements the Coq standard
library. *)
diff --git a/lib/Floats.v b/lib/Floats.v
index f4c5119..f11ead4 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -1,3 +1,18 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU General Public License as published by *)
+(* the Free Software Foundation, either version 2 of the License, or *)
+(* (at your option) any later version. This file is also distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
(** Axiomatization of floating-point numbers. *)
(** In contrast with what we do with machine integers, we do not bother
diff --git a/lib/Inclusion.v b/lib/Inclusion.v
index 15e37c4..728a725 100644
--- a/lib/Inclusion.v
+++ b/lib/Inclusion.v
@@ -1,3 +1,15 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
(** Tactics to reason about list inclusion. *)
(** This file (contributed by Laurence Rideau) defines a tactic [in_tac]
diff --git a/lib/Integers.v b/lib/Integers.v
index a3240e8..2d548fb 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -1,3 +1,18 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU General Public License as published by *)
+(* the Free Software Foundation, either version 2 of the License, or *)
+(* (at your option) any later version. This file is also distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
(** Formalizations of integers modulo $2^32$ #2<sup>32</sup>#. *)
Require Import Coqlib.
diff --git a/lib/Iteration.v b/lib/Iteration.v
index 85c5ded..cabe5b8 100644
--- a/lib/Iteration.v
+++ b/lib/Iteration.v
@@ -1,3 +1,15 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
(* Bounded and unbounded iterators *)
Require Import Coqlib.
diff --git a/lib/Lattice.v b/lib/Lattice.v
index f796367..3c39006 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -1,3 +1,15 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
(** Constructions of semi-lattices. *)
Require Import Coqlib.
diff --git a/lib/Maps.v b/lib/Maps.v
index 238009b..4a346c6 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -1,3 +1,18 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU General Public License as published by *)
+(* the Free Software Foundation, either version 2 of the License, or *)
+(* (at your option) any later version. This file is also distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
(** Applicative finite maps are the main data structure used in this
project. A finite map associates data to keys. The two main operations
are [set k d m], which returns a map identical to [m] except that [d]
diff --git a/lib/Ordered.v b/lib/Ordered.v
index ad47314..4b1f4e0 100644
--- a/lib/Ordered.v
+++ b/lib/Ordered.v
@@ -1,3 +1,15 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
(** Constructions of ordered types, for use with the [FSet] functors
for finite sets. *)
diff --git a/lib/Parmov.v b/lib/Parmov.v
index fa31b67..2c7b82a 100644
--- a/lib/Parmov.v
+++ b/lib/Parmov.v
@@ -1,3 +1,20 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Laurence Rideau, INRIA Sophia-Antipolis-Méditerranée *)
+(* Bernard Paul Serpette, INRIA Sophia-Antipolis-Méditerranée *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the GNU General Public License as published by *)
+(* the Free Software Foundation, either version 2 of the License, or *)
+(* (at your option) any later version. This file is also distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
(** Translation of parallel moves into sequences of individual moves *)
(** The ``parallel move'' problem, also known as ``parallel assignment'',