From a99776e10e0b2198d2b811ad82631111fb450f8a Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 18 Mar 2020 12:14:26 +0100 Subject: Update headers in the whole code base. Add headers to a few files which were missing them. --- kernel/byterun/coq_float64.h | 10 ++++++++++ kernel/byterun/coq_uint63_emul.h | 10 ++++++++++ kernel/byterun/coq_uint63_native.h | 10 ++++++++++ kernel/cClosure.ml | 4 ++-- kernel/cClosure.mli | 4 ++-- kernel/cPrimitives.ml | 4 ++-- kernel/cPrimitives.mli | 4 ++-- kernel/cbytecodes.ml | 4 ++-- kernel/cbytecodes.mli | 4 ++-- kernel/cbytegen.ml | 4 ++-- kernel/cbytegen.mli | 4 ++-- kernel/cemitcodes.ml | 4 ++-- kernel/cemitcodes.mli | 4 ++-- kernel/constr.ml | 4 ++-- kernel/constr.mli | 4 ++-- kernel/context.ml | 4 ++-- kernel/context.mli | 4 ++-- kernel/conv_oracle.ml | 4 ++-- kernel/conv_oracle.mli | 4 ++-- kernel/cooking.ml | 4 ++-- kernel/cooking.mli | 4 ++-- kernel/csymtable.ml | 4 ++-- kernel/csymtable.mli | 4 ++-- kernel/declarations.ml | 4 ++-- kernel/declareops.ml | 4 ++-- kernel/declareops.mli | 4 ++-- kernel/entries.ml | 4 ++-- kernel/environ.ml | 4 ++-- kernel/environ.mli | 4 ++-- kernel/esubst.ml | 4 ++-- kernel/esubst.mli | 4 ++-- kernel/evar.ml | 4 ++-- kernel/evar.mli | 4 ++-- kernel/float64.ml | 4 ++-- kernel/float64.mli | 4 ++-- kernel/genOpcodeFiles.ml | 4 ++-- kernel/indTyping.ml | 4 ++-- kernel/indTyping.mli | 4 ++-- kernel/indtypes.ml | 4 ++-- kernel/indtypes.mli | 4 ++-- kernel/inductive.ml | 4 ++-- kernel/inductive.mli | 4 ++-- kernel/inferCumulativity.ml | 4 ++-- kernel/inferCumulativity.mli | 4 ++-- kernel/mod_subst.ml | 4 ++-- kernel/mod_subst.mli | 4 ++-- kernel/mod_typing.ml | 4 ++-- kernel/mod_typing.mli | 4 ++-- kernel/modops.ml | 4 ++-- kernel/modops.mli | 4 ++-- kernel/names.ml | 4 ++-- kernel/names.mli | 4 ++-- kernel/nativecode.ml | 4 ++-- kernel/nativecode.mli | 4 ++-- kernel/nativeconv.ml | 4 ++-- kernel/nativeconv.mli | 4 ++-- kernel/nativelambda.ml | 4 ++-- kernel/nativelambda.mli | 4 ++-- kernel/nativelib.ml | 4 ++-- kernel/nativelib.mli | 4 ++-- kernel/nativelibrary.ml | 4 ++-- kernel/nativelibrary.mli | 4 ++-- kernel/nativevalues.ml | 4 ++-- kernel/nativevalues.mli | 4 ++-- kernel/opaqueproof.ml | 4 ++-- kernel/opaqueproof.mli | 4 ++-- kernel/reduction.ml | 4 ++-- kernel/reduction.mli | 4 ++-- kernel/retroknowledge.ml | 4 ++-- kernel/retroknowledge.mli | 4 ++-- kernel/retypeops.ml | 4 ++-- kernel/retypeops.mli | 4 ++-- kernel/safe_typing.ml | 4 ++-- kernel/safe_typing.mli | 4 ++-- kernel/section.ml | 4 ++-- kernel/section.mli | 4 ++-- kernel/sorts.ml | 4 ++-- kernel/sorts.mli | 4 ++-- kernel/subtyping.ml | 4 ++-- kernel/subtyping.mli | 4 ++-- kernel/term.ml | 4 ++-- kernel/term.mli | 4 ++-- kernel/term_typing.ml | 4 ++-- kernel/term_typing.mli | 4 ++-- kernel/transparentState.ml | 4 ++-- kernel/transparentState.mli | 4 ++-- kernel/type_errors.ml | 4 ++-- kernel/type_errors.mli | 4 ++-- kernel/typeops.ml | 4 ++-- kernel/typeops.mli | 4 ++-- kernel/uGraph.ml | 4 ++-- kernel/uGraph.mli | 4 ++-- kernel/uint63.mli | 4 ++-- kernel/uint63_31.ml | 4 ++-- kernel/uint63_63.ml | 4 ++-- kernel/univ.ml | 4 ++-- kernel/univ.mli | 4 ++-- kernel/vars.ml | 4 ++-- kernel/vars.mli | 4 ++-- kernel/vconv.mli | 4 ++-- kernel/vm.ml | 4 ++-- kernel/vm.mli | 4 ++-- kernel/vmvalues.ml | 4 ++-- kernel/vmvalues.mli | 4 ++-- 104 files changed, 232 insertions(+), 202 deletions(-) (limited to 'kernel') 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 */ +/* 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 */ +/* > 1) diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index af08ea18c1..1316dfe069 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(*