aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun
diff options
context:
space:
mode:
authorThéo Zimmermann2020-03-18 12:14:26 +0100
committerThéo Zimmermann2020-03-18 12:15:43 +0100
commita99776e10e0b2198d2b811ad82631111fb450f8a (patch)
tree2613f665dafdb34f34ebac4a9447208bbc35a8f6 /kernel/byterun
parenta33323d54cf78762f7ba1afc39a2f5a5ddb67a57 (diff)
Update headers in the whole code base.
Add headers to a few files which were missing them.
Diffstat (limited to 'kernel/byterun')
-rw-r--r--kernel/byterun/coq_float64.h10
-rw-r--r--kernel/byterun/coq_uint63_emul.h10
-rw-r--r--kernel/byterun/coq_uint63_native.h10
3 files changed, 30 insertions, 0 deletions
diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.h
index c41079c8ff..84a3edf1c7 100644
--- a/kernel/byterun/coq_float64.h
+++ b/kernel/byterun/coq_float64.h
@@ -1,3 +1,13 @@
+/************************************************************************/
+/* * The Coq Proof Assistant / The Coq Development Team */
+/* v * Copyright INRIA, CNRS and contributors */
+/* <O___,, * (see version control and CREDITS file for authors & dates) */
+/* \VV/ **************************************************************/
+/* // * This file is distributed under the terms of the */
+/* * GNU Lesser General Public License Version 2.1 */
+/* * (see LICENSE file for the text of the license) */
+/************************************************************************/
+
#ifndef _COQ_FLOAT64_
#define _COQ_FLOAT64_
diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
index 143a6d098c..d92bbe87eb 100644
--- a/kernel/byterun/coq_uint63_emul.h
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -1,3 +1,13 @@
+/************************************************************************/
+/* * The Coq Proof Assistant / The Coq Development Team */
+/* v * Copyright INRIA, CNRS and contributors */
+/* <O___,, * (see version control and CREDITS file for authors & dates) */
+/* \VV/ **************************************************************/
+/* // * This file is distributed under the terms of the */
+/* * GNU Lesser General Public License Version 2.1 */
+/* * (see LICENSE file for the text of the license) */
+/************************************************************************/
+
# pragma once
# include <caml/callback.h>
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
index 5be7587091..27696e8856 100644
--- a/kernel/byterun/coq_uint63_native.h
+++ b/kernel/byterun/coq_uint63_native.h
@@ -1,3 +1,13 @@
+/************************************************************************/
+/* * The Coq Proof Assistant / The Coq Development Team */
+/* v * Copyright INRIA, CNRS and contributors */
+/* <O___,, * (see version control and CREDITS file for authors & dates) */
+/* \VV/ **************************************************************/
+/* // * This file is distributed under the terms of the */
+/* * GNU Lesser General Public License Version 2.1 */
+/* * (see LICENSE file for the text of the license) */
+/************************************************************************/
+
#define Is_uint63(v) (Is_long(v))
#define uint_of_value(val) (((uint64_t)(val)) >> 1)