diff options
464 files changed, 3250 insertions, 1 deletions
@@ -1,5 +1,13 @@ +####################################################################### +# v # The Coq Proof Assistant / The Coq Development Team # +# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # +# \VV/ ############################################################# +# // # This file is distributed under the terms of the # +# # GNU Lesser General Public License Version 2.1 # +####################################################################### + +# $Id$ -########################################################################### # Makefile for Coq # # To be used with GNU Make. diff --git a/Makefile.dep b/Makefile.dep index 2b2905033..30690facf 100644 --- a/Makefile.dep +++ b/Makefile.dep @@ -1,3 +1,10 @@ +####################################################################### +# v # The Coq Proof Assistant / The Coq Development Team # +# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # +# \VV/ ############################################################# +# // # This file is distributed under the terms of the # +# # GNU Lesser General Public License Version 2.1 # +####################################################################### # This Makefile is designed to make the .ml files corresponding to .ml4 files diff --git a/config/coq_config.mli b/config/coq_config.mli index d4c18da8b..4f8c8f6d6 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v index 9e0f23c2d..0f9668756 100644 --- a/contrib/extraction/Extraction.v +++ b/contrib/extraction/Extraction.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Declare ML Module "ocaml.cmo" "extraction.cmo". diff --git a/contrib/extraction/close_env.ml b/contrib/extraction/close_env.ml index 2b4c66da6..ab303b094 100644 --- a/contrib/extraction/close_env.ml +++ b/contrib/extraction/close_env.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/contrib/extraction/close_env.mli b/contrib/extraction/close_env.mli index 066bb2a6d..bf6940d1c 100644 --- a/contrib/extraction/close_env.mli +++ b/contrib/extraction/close_env.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index a6f46235b..6aa5b7977 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli index 4c1d492c1..df5a414a1 100644 --- a/contrib/extraction/extraction.mli +++ b/contrib/extraction/extraction.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/contrib/extraction/genpp.ml b/contrib/extraction/genpp.ml index 27390de44..55d80d846 100644 --- a/contrib/extraction/genpp.ml +++ b/contrib/extraction/genpp.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/contrib/extraction/genpp.mli b/contrib/extraction/genpp.mli index 1bd795c09..376b069d0 100644 --- a/contrib/extraction/genpp.mli +++ b/contrib/extraction/genpp.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index 525b8dc3d..95b81fe10 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/contrib/extraction/mlimport.ml b/contrib/extraction/mlimport.ml index 12e39d044..6fd5d8657 100644 --- a/contrib/extraction/mlimport.ml +++ b/contrib/extraction/mlimport.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/contrib/extraction/mlimport.mli b/contrib/extraction/mlimport.mli index 6e302989f..4fdb2e9ea 100644 --- a/contrib/extraction/mlimport.mli +++ b/contrib/extraction/mlimport.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index ba7d59e72..83189ec57 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli index be80e419a..ff8dce97f 100644 --- a/contrib/extraction/ocaml.mli +++ b/contrib/extraction/ocaml.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v index 2f06ad397..2d40d97f5 100644 --- a/contrib/extraction/test_extraction.v +++ b/contrib/extraction/test_extraction.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Extraction nat. diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v index 8c646ae08..6c4a6191b 100755 --- a/contrib/omega/Omega.v +++ b/contrib/omega/Omega.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (**************************************************************************) (* *) (* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) diff --git a/contrib/omega/OmegaSyntax.v b/contrib/omega/OmegaSyntax.v index af673b097..a7f67f181 100644 --- a/contrib/omega/OmegaSyntax.v +++ b/contrib/omega/OmegaSyntax.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (**************************************************************************) (* *) (* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) diff --git a/contrib/omega/Zcomplements.v b/contrib/omega/Zcomplements.v index c80823237..52607a4a0 100644 --- a/contrib/omega/Zcomplements.v +++ b/contrib/omega/Zcomplements.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/omega/Zlogarithm.v b/contrib/omega/Zlogarithm.v index 5d343880e..3d29e0503 100644 --- a/contrib/omega/Zlogarithm.v +++ b/contrib/omega/Zlogarithm.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/omega/Zpower.v b/contrib/omega/Zpower.v index 824012d12..c2585b3e0 100644 --- a/contrib/omega/Zpower.v +++ b/contrib/omega/Zpower.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 821c4b202..71bfbe290 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (**************************************************************************) (* *) (* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml index 86f1a2e33..6d78494a2 100755 --- a/contrib/omega/omega.ml +++ b/contrib/omega/omega.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (**************************************************************************) (* *) (* Omega: a solver of quantifier-free problems in Presburger Arithmetic *) diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v index 14d69e2b0..0dfb1f4e3 100644 --- a/contrib/ring/ArithRing.v +++ b/contrib/ring/ArithRing.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v index e7c995cf3..f97c81c40 100644 --- a/contrib/ring/Quote.v +++ b/contrib/ring/Quote.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v index b6f75a584..c94dce065 100644 --- a/contrib/ring/Ring.v +++ b/contrib/ring/Ring.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v index 6bb1f5aa9..762689985 100644 --- a/contrib/ring/Ring_abstract.v +++ b/contrib/ring/Ring_abstract.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v index 536d2d303..94b5093c7 100644 --- a/contrib/ring/Ring_normalize.v +++ b/contrib/ring/Ring_normalize.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v index c04eee57e..867ab22fb 100644 --- a/contrib/ring/Ring_theory.v +++ b/contrib/ring/Ring_theory.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/ZArithRing.v index a8adfe2f6..2de861176 100644 --- a/contrib/ring/ZArithRing.v +++ b/contrib/ring/ZArithRing.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index ac3af30b8..c82ccecb0 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 0e200313c..589c1580e 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/xml/Xml.v b/contrib/xml/Xml.v index 5c6b788aa..f1d91371e 100644 --- a/contrib/xml/Xml.v +++ b/contrib/xml/Xml.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (******************************************************************************) (* *) (* PROJECT HELM *) diff --git a/contrib/xml/xml.ml b/contrib/xml/xml.ml index 635e83f68..60e16ab19 100644 --- a/contrib/xml/xml.ml +++ b/contrib/xml/xml.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (******************************************************************************) (* *) (* PROJECT HELM *) diff --git a/contrib/xml/xml.mli b/contrib/xml/xml.mli index 0510d978d..fbdb584ee 100644 --- a/contrib/xml/xml.mli +++ b/contrib/xml/xml.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (******************************************************************************) (* *) (* PROJECT HELM *) diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 906cf8b07..392782727 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (******************************************************************************) (* *) (* PROJECT HELM *) diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli index 1c9b22070..0ddc01c9a 100644 --- a/contrib/xml/xmlcommand.mli +++ b/contrib/xml/xmlcommand.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (******************************************************************************) (* *) (* PROJECT HELM *) diff --git a/contrib/xml/xmlentries.ml b/contrib/xml/xmlentries.ml index ffa0d5fc7..093727f2f 100644 --- a/contrib/xml/xmlentries.ml +++ b/contrib/xml/xmlentries.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (******************************************************************************) (* *) (* PROJECT HELM *) diff --git a/dev/db_printers.ml b/dev/db_printers.ml index 6290297ff..1384a77f5 100644 --- a/dev/db_printers.ml +++ b/dev/db_printers.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) open Pp open Names diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 47fb4b48d..7ea96f474 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* Printers for the ocaml toplevel. *) diff --git a/kernel/closure.ml b/kernel/closure.ml index ac8ed32eb..541cd7d59 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/closure.mli b/kernel/closure.mli index b4001f077..ef01b73bb 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index f0be35882..2ad841d03 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 99327605b..f29503176 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 9de1866cc..da393b235 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 531a616ba..18566a0c3 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/kernel/environ.ml b/kernel/environ.ml index f88860935..d21d5b51c 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/environ.mli b/kernel/environ.mli index eba1e0979..953580b0f 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 0ab021e4c..7d24804cc 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/esubst.mli b/kernel/esubst.mli index ea5df0a28..284c2f32e 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/evd.ml b/kernel/evd.ml index 548f8b14a..9a4d5af6a 100644 --- a/kernel/evd.ml +++ b/kernel/evd.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/evd.mli b/kernel/evd.mli index 2353b6789..6c0e6a716 100644 --- a/kernel/evd.mli +++ b/kernel/evd.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 228e2bafa..e67aff002 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index d0e3a4cb0..f5a6ca236 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index f03b1ba14..9a8ed21d8 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index e1ee0a56f..00c0dfbdb 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml index c73fbd220..a92de9e60 100644 --- a/kernel/instantiate.ml +++ b/kernel/instantiate.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli index 9b083293a..14a4746ee 100644 --- a/kernel/instantiate.mli +++ b/kernel/instantiate.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/kernel/names.ml b/kernel/names.ml index 035a5d505..b4b6c4302 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/names.mli b/kernel/names.mli index 98e39fae9..6b817e683 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 7c244c280..a92fe89ee 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 794c49354..20435a1fc 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index cb85a9868..ec3b75523 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 474da34b8..90703ae96 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/kernel/sign.ml b/kernel/sign.ml index fc3e15f5e..dff7e1218 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/sign.mli b/kernel/sign.mli index ede431eb4..6180906cb 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/kernel/term.ml b/kernel/term.ml index 66f706895..99e41ae56 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/term.mli b/kernel/term.mli index 87a6c06f6..b160594f1 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index bf0a99ee3..387b7a930 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index c45fac721..e022be01d 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 694d9ae77..17f30408d 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index f06e65653..b2db98373 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/kernel/univ.ml b/kernel/univ.ml index 4ea2ded00..fc5e4ff23 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/kernel/univ.mli b/kernel/univ.mli index 2460ff15e..3aedf921e 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/lib/bij.ml b/lib/bij.ml index cd0acbabb..345867f34 100644 --- a/lib/bij.ml +++ b/lib/bij.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/bij.mli b/lib/bij.mli index 7e6d23e82..e67db5364 100644 --- a/lib/bij.mli +++ b/lib/bij.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/lib/bstack.ml b/lib/bstack.ml index c67f51092..c52b0e713 100644 --- a/lib/bstack.ml +++ b/lib/bstack.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/bstack.mli b/lib/bstack.mli index fc646f1a4..febf7850e 100644 --- a/lib/bstack.mli +++ b/lib/bstack.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/lib/dyn.ml b/lib/dyn.ml index 3d6d43f8c..0bbf773b9 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/dyn.mli b/lib/dyn.mli index 2c0587ee6..819f240b9 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/lib/edit.ml b/lib/edit.ml index 8d0b0aa27..ca41a0436 100644 --- a/lib/edit.ml +++ b/lib/edit.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/edit.mli b/lib/edit.mli index c86022e44..4f3b7803c 100644 --- a/lib/edit.mli +++ b/lib/edit.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/lib/explore.ml b/lib/explore.ml index b79f3e820..47a6687e5 100644 --- a/lib/explore.ml +++ b/lib/explore.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/lib/explore.mli b/lib/explore.mli index 5f484f8e6..6350feccb 100644 --- a/lib/explore.mli +++ b/lib/explore.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/lib/gmap.ml b/lib/gmap.ml index 52af882b3..83a8cc3d6 100644 --- a/lib/gmap.ml +++ b/lib/gmap.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) (* Maps using the generic comparison function of ocaml. Code borrowed from diff --git a/lib/gmap.mli b/lib/gmap.mli index a73bdba51..107e5e2d9 100644 --- a/lib/gmap.mli +++ b/lib/gmap.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/lib/gmapl.ml b/lib/gmapl.ml index 6295c4099..013b91ac3 100644 --- a/lib/gmapl.ml +++ b/lib/gmapl.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/gmapl.mli b/lib/gmapl.mli index 23c77851b..f44fad27c 100644 --- a/lib/gmapl.mli +++ b/lib/gmapl.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/lib/gset.ml b/lib/gset.ml index 1dc710be0..e18e01187 100644 --- a/lib/gset.ml +++ b/lib/gset.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/gset.mli b/lib/gset.mli index 125fbe442..f6f2a95ea 100644 --- a/lib/gset.mli +++ b/lib/gset.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/lib/hashcons.ml b/lib/hashcons.ml index 55405a7aa..45ef9a0f5 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/hashcons.mli b/lib/hashcons.mli index 07dd8bc2b..aea23900b 100644 --- a/lib/hashcons.mli +++ b/lib/hashcons.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/lib/options.ml b/lib/options.ml index a4e00c6b3..82ee767d3 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/options.mli b/lib/options.mli index 576794f39..61372bfe5 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/pp.mli b/lib/pp.mli index 96ef3d3de..d0730044c 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/lib/pp_control.ml b/lib/pp_control.ml index 34ebf76fc..2e8476790 100644 --- a/lib/pp_control.ml +++ b/lib/pp_control.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/pp_control.mli b/lib/pp_control.mli index b6d6132e0..2551726df 100644 --- a/lib/pp_control.mli +++ b/lib/pp_control.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/lib/profile.ml b/lib/profile.ml index 8a90abf5d..825b792d7 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/profile.mli b/lib/profile.mli index 647aaea44..8d4105cf6 100644 --- a/lib/profile.mli +++ b/lib/profile.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/stamps.ml b/lib/stamps.ml index 0441d2de1..ab1b608a5 100644 --- a/lib/stamps.ml +++ b/lib/stamps.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/stamps.mli b/lib/stamps.mli index 40a83feb6..a85d7174d 100644 --- a/lib/stamps.mli +++ b/lib/stamps.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/lib/system.ml b/lib/system.ml index db478d9e3..cf48f0e4b 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/system.mli b/lib/system.mli index a9ffd5b63..5c893eb30 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/lib/tlm.ml b/lib/tlm.ml index d16353f1e..fca2db5ec 100644 --- a/lib/tlm.ml +++ b/lib/tlm.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/tlm.mli b/lib/tlm.mli index f04639750..1a6f61124 100644 --- a/lib/tlm.mli +++ b/lib/tlm.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/lib/util.ml b/lib/util.ml index 29273b169..5e10091e3 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/lib/util.mli b/lib/util.mli index 274d97af4..d46672a60 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/library/declare.ml b/library/declare.ml index f0f2790a5..f7388133c 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/library/declare.mli b/library/declare.mli index 6c47e3a52..bde04bfba 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/library/global.ml b/library/global.ml index faca388aa..b4f45ad69 100644 --- a/library/global.ml +++ b/library/global.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/library/global.mli b/library/global.mli index da0386be1..c463bd153 100644 --- a/library/global.mli +++ b/library/global.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/library/goptions.ml b/library/goptions.ml index 59d0543e2..8c0c08cef 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/library/goptions.mli b/library/goptions.mli index 08f5262eb..012967561 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/library/impargs.ml b/library/impargs.ml index 8dc025e59..4d12d9ac1 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/library/impargs.mli b/library/impargs.mli index bd5f6024a..9b8d0616d 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/library/indrec.ml b/library/indrec.ml index 65abfb158..c02cb35e2 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/library/indrec.mli b/library/indrec.mli index 8a47c1fae..4f3cd5ee7 100644 --- a/library/indrec.mli +++ b/library/indrec.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/library/lib.ml b/library/lib.ml index 10fd9b965..c46a3833b 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/library/lib.mli b/library/lib.mli index 668a65adf..f8a126cce 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/library/libobject.ml b/library/libobject.ml index c644cc4eb..4f63109bf 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/library/libobject.mli b/library/libobject.mli index 7b63af380..2f68f3b27 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/library/library.ml b/library/library.ml index e58f71659..b30852e7d 100644 --- a/library/library.ml +++ b/library/library.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/library/library.mli b/library/library.mli index 43fa04e8b..e5ad55e48 100644 --- a/library/library.mli +++ b/library/library.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/library/nametab.ml b/library/nametab.ml index 253483791..4272bda59 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/library/nametab.mli b/library/nametab.mli index a62385bb6..5e867c11d 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/library/states.ml b/library/states.ml index 5a4983a80..6bd8b7d64 100644 --- a/library/states.ml +++ b/library/states.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/library/states.mli b/library/states.mli index 5ff97d103..9139c860b 100644 --- a/library/states.mli +++ b/library/states.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/library/summary.ml b/library/summary.ml index 8fbd5efe4..c315e0cd2 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/library/summary.mli b/library/summary.mli index feca53fe3..d381543b9 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/ast.ml b/parsing/ast.ml index a438bdeb4..b87037127 100755 --- a/parsing/ast.ml +++ b/parsing/ast.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/parsing/ast.mli b/parsing/ast.mli index 160f0928c..0379ba305 100755 --- a/parsing/ast.mli +++ b/parsing/ast.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/astterm.ml b/parsing/astterm.ml index ea1c307b6..6a527d43e 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/parsing/astterm.mli b/parsing/astterm.mli index cf2cbfd51..6f7d400fe 100644 --- a/parsing/astterm.mli +++ b/parsing/astterm.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/coqast.ml b/parsing/coqast.ml index 0f0dcda29..81df802bc 100644 --- a/parsing/coqast.ml +++ b/parsing/coqast.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/parsing/coqast.mli b/parsing/coqast.mli index 38803b5ae..255611c46 100644 --- a/parsing/coqast.mli +++ b/parsing/coqast.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/coqlib.ml b/parsing/coqlib.ml index d7e8efa20..0aae508e5 100644 --- a/parsing/coqlib.ml +++ b/parsing/coqlib.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/parsing/coqlib.mli b/parsing/coqlib.mli index c835eeffa..13699a242 100644 --- a/parsing/coqlib.mli +++ b/parsing/coqlib.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 166d43536..aa9ab17aa 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index 47e477fc5..83dc3ce65 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml index ef9b4feec..ba6e8614e 100644 --- a/parsing/esyntax.ml +++ b/parsing/esyntax.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli index fe8542a51..8f7fbce75 100644 --- a/parsing/esyntax.mli +++ b/parsing/esyntax.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/extend.ml4 b/parsing/extend.ml4 index 1f6c36753..f5969f4b2 100644 --- a/parsing/extend.ml4 +++ b/parsing/extend.ml4 @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i camlp4deps: "parsing/grammar.cma" i*) diff --git a/parsing/extend.mli b/parsing/extend.mli index 086d1b2eb..00ffb2097 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index b4d380c80..10fd8c67c 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i camlp4deps: "parsing/grammar.cma" i*) diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4 index d464e2f47..52c35ce04 100644 --- a/parsing/g_cases.ml4 +++ b/parsing/g_cases.ml4 @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i camlp4deps: "parsing/grammar.cma" i*) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index e4cbc2c1d..709cc1030 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i camlp4deps: "parsing/grammar.cma" i*) diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4 index e9f47b085..4eec7bb5f 100644 --- a/parsing/g_minicoq.ml4 +++ b/parsing/g_minicoq.ml4 @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i camlp4deps: "parsing/grammar.cma" i*) diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli index 7ebd65770..f3c60cedd 100644 --- a/parsing/g_minicoq.mli +++ b/parsing/g_minicoq.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml index a4c9d9082..6b67c1c0a 100644 --- a/parsing/g_natsyntax.ml +++ b/parsing/g_natsyntax.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/parsing/g_natsyntax.mli b/parsing/g_natsyntax.mli index f9b7b51d1..91596ef5c 100644 --- a/parsing/g_natsyntax.mli +++ b/parsing/g_natsyntax.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 7a09453af..05f4dc42e 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index d176a05aa..efd6a5de2 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i camlp4deps: "parsing/grammar.cma" i*) diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml index b9902e103..a6ba6cb61 100644 --- a/parsing/g_rsyntax.ml +++ b/parsing/g_rsyntax.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) open Coqast open Ast open Pp diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 4595c81b8..f26034c91 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i camlp4deps: "parsing/grammar.cma" i*) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 431b687f6..f1cae2458 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i camlp4deps: "parsing/grammar.cma" i*) diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml index 26f946d03..96f9bc611 100644 --- a/parsing/g_zsyntax.ml +++ b/parsing/g_zsyntax.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/parsing/g_zsyntax.mli b/parsing/g_zsyntax.mli index f04d6a151..a8370f630 100644 --- a/parsing/g_zsyntax.mli +++ b/parsing/g_zsyntax.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index adc15c8a7..570e04711 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/lexer.mli b/parsing/lexer.mli index b7dc6e25d..9b0e3bbd8 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 2d451839f..6792ae044 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 79d33a98b..0ad8a73c4 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 1e45d0ea2..ef46a0399 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/parsing/pretty.mli b/parsing/pretty.mli index 7b4ea47e8..c5071367b 100644 --- a/parsing/pretty.mli +++ b/parsing/pretty.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/printer.ml b/parsing/printer.ml index a325f1a8b..dc77058d1 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/parsing/printer.mli b/parsing/printer.mli index fe456f047..9f0d84e6d 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 256b48d6c..0b6e92a43 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/parsing/search.ml b/parsing/search.ml index fc2100a6a..88ab104ef 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/parsing/search.mli b/parsing/search.mli index 96f64b7ce..4cd8e85c2 100644 --- a/parsing/search.mli +++ b/parsing/search.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/parsing/termast.ml b/parsing/termast.ml index 335c2bcf4..796798be9 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/parsing/termast.mli b/parsing/termast.mli index 35a7349d8..df18bc27e 100644 --- a/parsing/termast.mli +++ b/parsing/termast.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 2689772ce..3e530b672 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 310842b6d..acd9f3089 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 15a50bcc4..461100816 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 08e067f5a..778eebff7 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 630a8bb31..4cd71d09d 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 4ccf02b1f..fc0cc1de2 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index bd25f9351..5f8e90cb2 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) open Util diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index e636f2fbd..f7ea9352b 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index ab6104f96..877dca8c9 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 6d19c624a..f68c0356f 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 82746d287..7a1423c3c 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index f1a247b45..9b45a5094 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d7df2507c..c34e07bac 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 772841e13..53f4cb9e3 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/multcase.mli b/pretyping/multcase.mli index 41cf5561e..a71fdf0be 100644 --- a/pretyping/multcase.mli +++ b/pretyping/multcase.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index b83019b45..01ccd27fa 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index 0bce54e74..e687e5cbc 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 985b7975c..f35b1b10b 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index ba8c0e4e7..717191aa8 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 806a84d66..0e2974b0b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index d28732941..f0bc559ae 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index f6fc0dbd6..e7b5bd5ef 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 18845d8b1..18e3b1a1f 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 6db3545ce..c8c43a245 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 097eb25b8..25e024a6c 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 657f3d1e0..43e0a91f9 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 5eee11d19..2e32601d9 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml index 1e63907a4..6a171d7c4 100644 --- a/pretyping/syntax_def.ml +++ b/pretyping/syntax_def.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/pretyping/syntax_def.mli b/pretyping/syntax_def.mli index cbe1ba7e5..1a884300c 100644 --- a/pretyping/syntax_def.mli +++ b/pretyping/syntax_def.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index d942a6611..f65176602 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index df3a0b973..4d248983f 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index afdaf5823..c39197af7 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 8fae1cd41..29cf0da62 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 31555eaa8..0fd86d9a3 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/proofs/clenv.mli b/proofs/clenv.mli index dd8e9c31e..59d61a567 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 40c1f2906..ca6e2108c 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 24ab10970..bddbc2b35 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/proofs/logic.ml b/proofs/logic.ml index 0f1d2c84c..b3800da28 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/proofs/logic.mli b/proofs/logic.mli index 8591e3367..5381cffc4 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 7ac4c07b0..777870249 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 128c2b265..3ca4ea654 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 4a8f8dfc6..b6867ef89 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index a76eba1cb..d579190b3 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 3f5dbaeea..6a22de3e6 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i*) open Environ open Evd diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 3a9f32b63..1c9605b2e 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index e9c214753..0752b2ca9 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 31dc12851..59c5e4e4e 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index cd7252c44..6b7d118ae 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli index 9232d598d..fca4da9d4 100644 --- a/proofs/tacinterp.mli +++ b/proofs/tacinterp.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 5ba5e0f96..81aa16c6f 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 456398fc5..6deb24391 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index d9c5d528a..0cdf49c70 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) open Ast open Pp open Printer diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index fffe58348..aa386762b 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/scripts/coqc.ml b/scripts/coqc.ml index 3ed173455..d807d5d39 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index b18733f74..4b24cfd17 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/states/MakeInitial.v b/states/MakeInitial.v index 151306194..55b824e54 100644 --- a/states/MakeInitial.v +++ b/states/MakeInitial.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Require Export Prelude. Require Export Logic_Type. Require Export Logic_TypeSyntax. diff --git a/syntax/MakeBare.v b/syntax/MakeBare.v index bb12e7058..17a5e04a6 100644 --- a/syntax/MakeBare.v +++ b/syntax/MakeBare.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Load PPConstr. Load PPCases. Load PPTactic. diff --git a/syntax/PPCases.v b/syntax/PPCases.v index 5f05b9d27..f8b4eb947 100644 --- a/syntax/PPCases.v +++ b/syntax/PPCases.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v index 1c8026794..8590ee7c1 100755 --- a/syntax/PPConstr.v +++ b/syntax/PPConstr.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v index 11f5167ca..a84a81f6e 100644 --- a/syntax/PPTactic.v +++ b/syntax/PPTactic.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/AutoRewrite.v b/tactics/AutoRewrite.v index 2810f4cc5..74e6d4d26 100644 --- a/tactics/AutoRewrite.v +++ b/tactics/AutoRewrite.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Declare ML Module "autorewrite". Grammar vernac orient : ast := diff --git a/tactics/EAuto.v b/tactics/EAuto.v index cb075aa79..e1ac47ddd 100644 --- a/tactics/EAuto.v +++ b/tactics/EAuto.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* The Calculus of Inductive Constructions *) (* *) diff --git a/tactics/EqDecide.v b/tactics/EqDecide.v index 4fa3c2f06..05305d1b2 100644 --- a/tactics/EqDecide.v +++ b/tactics/EqDecide.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* EqDecide.v *) (* A tactic for deciding propositional equality on inductive types *) diff --git a/tactics/Equality.v b/tactics/Equality.v index 057e6f900..a6e138857 100644 --- a/tactics/Equality.v +++ b/tactics/Equality.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$: *) diff --git a/tactics/Inv.v b/tactics/Inv.v index 62c77dc8a..36316ec81 100644 --- a/tactics/Inv.v +++ b/tactics/Inv.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id: *) diff --git a/tactics/Refine.v b/tactics/Refine.v index fe421497f..fb73d66ee 100644 --- a/tactics/Refine.v +++ b/tactics/Refine.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/Tauto.v b/tactics/Tauto.v index c6283109c..e6b8b5e83 100644 --- a/tactics/Tauto.v +++ b/tactics/Tauto.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 72a371267..721ad2cf3 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/auto.mli b/tactics/auto.mli index 2e89462ad..bff61a849 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index f57b3f32c..a8dc18b76 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) open Ast open Coqast open Equality diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 2e291e542..ce9265866 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index e238f5f79..2b7b78d69 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index ef1aaa50a..6cccb76dd 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 6497287ab..a40a74843 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli index 2cbf9a827..4879bafc7 100644 --- a/tactics/dhyp.mli +++ b/tactics/dhyp.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/dn.ml b/tactics/dn.ml index b53fb2661..0e8542774 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/dn.mli b/tactics/dn.mli index c39ab011c..da32f853c 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 931a7a555..2a13a9718 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/elim.ml b/tactics/elim.ml index 34aab19ad..c61cdb077 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/elim.mli b/tactics/elim.mli index af7d17506..e2b9a75e3 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 1897a8ba6..ae2d8a4a5 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/equality.ml b/tactics/equality.ml index 726131dee..c64a86949 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/equality.mli b/tactics/equality.mli index d1543e47e..1735ebf1a 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 48b29ea5e..2c4f80b74 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 2c45e831e..517889c16 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index ba519cb2f..2a2b46cba 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 306a74043..f1a758d8b 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/inv.ml b/tactics/inv.ml index 9b81e87e6..57d6ca701 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/inv.mli b/tactics/inv.mli index f09744c56..ed0dc1de0 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 8ca683188..3759093f1 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index 918313d0f..abd201a3b 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli index 7b7da16ef..b056e41cf 100644 --- a/tactics/nbtermdn.mli +++ b/tactics/nbtermdn.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/refine.ml b/tactics/refine.ml index dadda64de..9492e8eb2 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/refine.mli b/tactics/refine.mli index 86d4e9c34..f50ea12b4 100644 --- a/tactics/refine.mli +++ b/tactics/refine.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml index 852b0ff83..d89f36e6b 100644 --- a/tactics/tacentries.ml +++ b/tactics/tacentries.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli index e12ed0e8c..8c6cfebaf 100644 --- a/tactics/tacentries.mli +++ b/tactics/tacentries.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index bef40065f..787413d92 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index e13c4758c..aeaae6b4e 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 424b785bc..b592fb759 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index c81e1436f..e17806ab7 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 7ca436293..a10eb70a9 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i camlp4deps: "parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo" i*) diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 4f3ea7522..4de0a8e46 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/termdn.mli b/tactics/termdn.mli index 044cbf4ff..fa60731f7 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml index b8bcb18ec..1255cad54 100644 --- a/tactics/wcclausenv.ml +++ b/tactics/wcclausenv.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli index fedea8470..b7de77101 100644 --- a/tactics/wcclausenv.mli +++ b/tactics/wcclausenv.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v index 62a34dbd4..0a4b51506 100644 --- a/test-suite/bench/lists-100.v +++ b/test-suite/bench/lists-100.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Inductive list0 : Set := nil0 : list0 | cons0 : Set -> list0 -> list0. Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1. Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2. diff --git a/test-suite/bench/lists_100.v b/test-suite/bench/lists_100.v index 62a34dbd4..0a4b51506 100644 --- a/test-suite/bench/lists_100.v +++ b/test-suite/bench/lists_100.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Inductive list0 : Set := nil0 : list0 | cons0 : Set -> list0 -> list0. Inductive list1 : Set := nil1 : list1 | cons1 : Set -> list1 -> list1. Inductive list2 : Set := nil2 : list2 | cons2 : Set -> list2 -> list2. diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v index 3e8bbeeb1..8af5c310a 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (**** Tactics Tauto and Intuition ****) (**** Tauto: diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v index ac6511bdf..9f3865293 100644 --- a/test-suite/failure/clash_cons.v +++ b/test-suite/failure/clash_cons.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* Teste la verification d'unicite des noms de constr *) diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v index 5d53cb7ef..cf6593cb3 100644 --- a/test-suite/failure/fixpoint1.v +++ b/test-suite/failure/fixpoint1.v @@ -1,2 +1,9 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Fixpoint PreParadox [u:unit] : False := (PreParadox u). Definition Paradox := (PreParadox tt).
\ No newline at end of file diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v index 3f6206c76..1427cec86 100644 --- a/test-suite/failure/illtype1.v +++ b/test-suite/failure/illtype1.v @@ -1 +1,8 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Check (S S). diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v index 09025197c..4c18c5c04 100644 --- a/test-suite/failure/positivity.v +++ b/test-suite/failure/positivity.v @@ -1 +1,8 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Inductive t:Set := c: (t -> nat) -> t. diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v index 0c821906e..d46147843 100644 --- a/test-suite/failure/redef.v +++ b/test-suite/failure/redef.v @@ -1,2 +1,9 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Definition toto := Set. Definition toto := Set. diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v index fe5bebc21..2f3069a1c 100644 --- a/test-suite/failure/search.v +++ b/test-suite/failure/search.v @@ -1 +1,8 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) SearchPattern ? = ? outside n_existe_pas. diff --git a/test-suite/success/Apply.v b/test-suite/success/Apply.v index a6aec8479..a1150fb4b 100644 --- a/test-suite/success/Apply.v +++ b/test-suite/success/Apply.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* This needs unification on type *) diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index bf2c3f9eb..3dcfbefb3 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* Pattern-matching when non inductive terms occur *) diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index 2c9fc7ada..b8d06acb5 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* Compiling the theories allows to test parsing and typing but not printing *) (* This file tests that pretty-printing does not fail *) (* Test of exact output is not specified *) diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v index 0dbed8ffa..af840d4a6 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (**** Tactics Tauto and Intuition ****) (**** Tauto: diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 7681c8aa4..8a5e146d4 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Require PolyList. Parameter in_list : (list nat*nat)->nat->Prop. diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index f118bc830..434ec5464 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Inductive T : Set := A: T | B :T->T. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 188ce73d5..6d52ec4c6 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* The "?" of cons and eq should be inferred *) Variable list:Set -> Set. Variable cons:(T:Set) T -> (list T) -> (list T). diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v index 3834fc0f5..c26cb16f9 100644 --- a/test-suite/success/fix.v +++ b/test-suite/success/fix.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* Ancien bug signale par Laurent Thery sur la condition de garde *) Require Import Bool. diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v index af31940db..2159c36b6 100644 --- a/test-suite/success/inds_type_sec.v +++ b/test-suite/success/inds_type_sec.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Section S. Inductive T [U:Type] : Set := c : U -> (T U). End S. diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index cffc8ba7a..6ab77e008 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* Teste des definitions inductives imbriquees *) Require PolyList. diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index 61d984eb4..7ef885148 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* Definition mutuellement inductive et dependante *) Require Export PolyList. diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 59adcff23..9c79507f7 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* Test le Hint Unfold sur des var locales *) Section toto. diff --git a/test-suite/tactics/TestRefine.v b/test-suite/tactics/TestRefine.v index 1643c44ca..b8c0146e8 100644 --- a/test-suite/tactics/TestRefine.v +++ b/test-suite/tactics/TestRefine.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* Petit bench vite fait, mal fait *) diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index d5b4610a6..7917f1582 100755 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 70307311b..8513e6b52 100755 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index d1415318a..a43941755 100755 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 0e49083b9..8ef796eef 100755 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v index c6ea0a6f2..24f4ba36c 100755 --- a/theories/Arith/Div.v +++ b/theories/Arith/Div.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index f5e7ebb34..25b5d21da 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index c97a9aaa4..cd3e404cd 100755 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Euclid_def.v b/theories/Arith/Euclid_def.v index 292816f45..a30b93caf 100755 --- a/theories/Arith/Euclid_def.v +++ b/theories/Arith/Euclid_def.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Euclid_proof.v b/theories/Arith/Euclid_proof.v index b8863ad65..e4034b0a5 100755 --- a/theories/Arith/Euclid_proof.v +++ b/theories/Arith/Euclid_proof.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index a79a4d267..2d142cdc8 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v index 904aac7bd..f2e27e7bf 100755 --- a/theories/Arith/Gt.v +++ b/theories/Arith/Gt.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index 66c73ff82..7766d3d7e 100755 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index 4c5167e82..aa4ad4950 100755 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 9f5cf5f63..8f9eb5ecd 100755 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index 4594aa74d..29a978070 100755 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index fe80384aa..ff38eef69 100755 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index d57ec2d51..913d6dd37 100755 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index f1bc532aa..2f96112c3 100755 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 225ebeff5..3e8d174c8 100755 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 7826e3882..68475a57e 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index a713c0409..59278ec11 100755 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index 8d86c6315..f4c4d4cb4 100755 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index a7d600289..749accdd4 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index 3c62e7ab0..b36fc94d5 100755 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 19760df51..ca5e2ef99 100755 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v index 914f86761..2f0eb5cf2 100644 --- a/theories/Init/DatatypesSyntax.v +++ b/theories/Init/DatatypesSyntax.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index ec1d850e0..2c5c0f569 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v index de17836e0..fd394c1aa 100644 --- a/theories/Init/LogicSyntax.v +++ b/theories/Init/LogicSyntax.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index b78fcb93b..08a054900 100755 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v index 5064ddcec..a1cce77a5 100644 --- a/theories/Init/Logic_TypeSyntax.v +++ b/theories/Init/Logic_TypeSyntax.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 4efc6c693..fc99d1a48 100755 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index c80278aaa..8f8fa294e 100755 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 53d3dd136..c86c38dd5 100755 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v index e48ba77f6..bae1b2a1a 100644 --- a/theories/Init/SpecifSyntax.v +++ b/theories/Init/SpecifSyntax.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 454ca5dff..eb0be95cf 100755 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 034868607..50b15b1c9 100755 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index 3c083aa97..565a32404 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v index 1a0211d54..7c11eb489 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v index a19a3dcc1..7776b7d2e 100644 --- a/theories/Lists/PolyListSyntax.v +++ b/theories/Lists/PolyListSyntax.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 297a888eb..5bc9dc97e 100755 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v index f3f87c40e..a57681df6 100755 --- a/theories/Lists/TheoryList.v +++ b/theories/Lists/TheoryList.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v index e4406a65f..a9c63f0bf 100755 --- a/theories/Logic/Classical.v +++ b/theories/Logic/Classical.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v index 3b4e17041..098ae33fc 100755 --- a/theories/Logic/Classical_Pred_Set.v +++ b/theories/Logic/Classical_Pred_Set.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v index 2f3b331cb..c5c105378 100755 --- a/theories/Logic/Classical_Pred_Type.v +++ b/theories/Logic/Classical_Pred_Type.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index f9afd26b0..826d068ae 100755 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v index c679f549c..ca63074d8 100755 --- a/theories/Logic/Classical_Type.v +++ b/theories/Logic/Classical_Type.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v index 6f19c543b..01702cd16 100755 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 6205fc603..0b5c56ae1 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Num/AddProps.v b/theories/Num/AddProps.v index 87fba8eba..cc48a8744 100644 --- a/theories/Num/AddProps.v +++ b/theories/Num/AddProps.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Require Export Axioms. diff --git a/theories/Num/Axioms.v b/theories/Num/Axioms.v index 7e65fc947..c9ada6ebc 100644 --- a/theories/Num/Axioms.v +++ b/theories/Num/Axioms.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id: i*) (*s Axioms for the basic numerical operations *) diff --git a/theories/Num/Definitions.v b/theories/Num/Definitions.v index defb12897..2b908f5cd 100644 --- a/theories/Num/Definitions.v +++ b/theories/Num/Definitions.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id $ i*) (*s diff --git a/theories/Num/DiscrAxioms.v b/theories/Num/DiscrAxioms.v index 42e58cd3c..83b2e42f4 100644 --- a/theories/Num/DiscrAxioms.v +++ b/theories/Num/DiscrAxioms.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) Require Export Params. diff --git a/theories/Num/DiscrProps.v b/theories/Num/DiscrProps.v index 7c84d2b35..5554357e8 100644 --- a/theories/Num/DiscrProps.v +++ b/theories/Num/DiscrProps.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) Require Export DiscrAxioms. diff --git a/theories/Num/GeAxioms.v b/theories/Num/GeAxioms.v index d5d2375e9..f24247975 100644 --- a/theories/Num/GeAxioms.v +++ b/theories/Num/GeAxioms.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id: i*) Require Export Axioms. Require Export LtProps. diff --git a/theories/Num/GeProps.v b/theories/Num/GeProps.v index e69de29bb..b5bc074d1 100644 --- a/theories/Num/GeProps.v +++ b/theories/Num/GeProps.v @@ -0,0 +1,7 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) diff --git a/theories/Num/GtAxioms.v b/theories/Num/GtAxioms.v index 9a54a0988..548d43cdf 100644 --- a/theories/Num/GtAxioms.v +++ b/theories/Num/GtAxioms.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id: i*) Require Export Axioms. Require Export LeProps. diff --git a/theories/Num/GtProps.v b/theories/Num/GtProps.v index e69de29bb..b5bc074d1 100644 --- a/theories/Num/GtProps.v +++ b/theories/Num/GtProps.v @@ -0,0 +1,7 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) diff --git a/theories/Num/LeAxioms.v b/theories/Num/LeAxioms.v index b71682e4f..668c4677d 100644 --- a/theories/Num/LeAxioms.v +++ b/theories/Num/LeAxioms.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id: i*) Require Export Axioms. Require Export LtProps. diff --git a/theories/Num/LeProps.v b/theories/Num/LeProps.v index 68f782e63..c476bb206 100644 --- a/theories/Num/LeProps.v +++ b/theories/Num/LeProps.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Require Export LtProps. Require Export LeAxioms. diff --git a/theories/Num/LtProps.v b/theories/Num/LtProps.v index aeff45f29..490fbbb12 100644 --- a/theories/Num/LtProps.v +++ b/theories/Num/LtProps.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) Require Export Axioms. Require Export AddProps. diff --git a/theories/Num/NSyntax.v b/theories/Num/NSyntax.v index 117832c01..488f900e5 100644 --- a/theories/Num/NSyntax.v +++ b/theories/Num/NSyntax.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*s Syntax for arithmetic *) diff --git a/theories/Num/OppAxioms.v b/theories/Num/OppAxioms.v index e69de29bb..b5bc074d1 100644 --- a/theories/Num/OppAxioms.v +++ b/theories/Num/OppAxioms.v @@ -0,0 +1,7 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) diff --git a/theories/Num/OppProps.v b/theories/Num/OppProps.v index e69de29bb..b5bc074d1 100644 --- a/theories/Num/OppProps.v +++ b/theories/Num/OppProps.v @@ -0,0 +1,7 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) diff --git a/theories/Num/SubProps.v b/theories/Num/SubProps.v index e69de29bb..b5bc074d1 100644 --- a/theories/Num/SubProps.v +++ b/theories/Num/SubProps.v @@ -0,0 +1,7 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index d3f0464ee..e766b35d7 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 38c423938..52b267610 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index 91c3e5409..0562215fe 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 6b2106630..9edaa4d37 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index ecaa7b4ca..055cf58f8 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index 680a18ab9..3090feef0 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v index 3af2faa4c..f623504aa 100644 --- a/theories/Reals/Reals.v +++ b/theories/Reals/Reals.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index c030cb4a0..3e92a2a2f 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 465dfd7a4..79fe3bb01 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v index 5f8b0d7a3..68b745654 100644 --- a/theories/Reals/Rsyntax.v +++ b/theories/Reals/Rsyntax.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) Require Export Rdefinitions. diff --git a/theories/Reals/TypeSyntax.v b/theories/Reals/TypeSyntax.v index 9b68928ba..3d3ad4d7a 100644 --- a/theories/Reals/TypeSyntax.v +++ b/theories/Reals/TypeSyntax.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v index 4f07dad8d..c5f3f7ddb 100755 --- a/theories/Relations/Newman.v +++ b/theories/Relations/Newman.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index e3da5130f..412533d8d 100755 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v index 9d32ae9be..afd9e7588 100755 --- a/theories/Relations/Relation_Definitions.v +++ b/theories/Relations/Relation_Definitions.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index 1944b60cd..d5b592628 100755 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index f11537a6e..ff17058f4 100755 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v index fb503386c..86b121883 100755 --- a/theories/Relations/Rstar.v +++ b/theories/Relations/Rstar.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v index 2cd2df78a..0350f6114 100755 --- a/theories/Sets/Classical_sets.v +++ b/theories/Sets/Classical_sets.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v index 3c8023cae..03e6b5f01 100755 --- a/theories/Sets/Constructive_sets.v +++ b/theories/Sets/Constructive_sets.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index e367ac32b..7e828e75f 100755 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index 68591b792..42cf98496 100755 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index 5e721d8a0..0d1e9ff41 100755 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v index b19fba44a..52ce9e651 100755 --- a/theories/Sets/Finite_sets_facts.v +++ b/theories/Sets/Finite_sets_facts.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index e7dc2184e..680b3f7fb 100755 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v index b529775aa..02ea826f4 100755 --- a/theories/Sets/Infinite_sets.v +++ b/theories/Sets/Infinite_sets.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index 21767405c..03572d760 100755 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index ae0d77035..5c37b0fd9 100755 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index a1c1639f0..0f117e62d 100755 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index 8b4d0b7a4..baf28a53f 100755 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index 9b2f57809..7caaacf97 100755 --- a/theories/Sets/Powerset.v +++ b/theories/Sets/Powerset.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v index 02a9b750d..bd46f6402 100755 --- a/theories/Sets/Powerset_Classical_facts.v +++ b/theories/Sets/Powerset_Classical_facts.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index b886f1211..4894ac486 100755 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v index 1e7e760a1..a7d1b3b17 100755 --- a/theories/Sets/Relations_1.v +++ b/theories/Sets/Relations_1.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index 3c9609182..ddcc433b8 100755 --- a/theories/Sets/Relations_1_facts.v +++ b/theories/Sets/Relations_1_facts.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v index 28cc6a5f6..e0de488b8 100755 --- a/theories/Sets/Relations_2.v +++ b/theories/Sets/Relations_2.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v index 05f3753be..ec90057aa 100755 --- a/theories/Sets/Relations_2_facts.v +++ b/theories/Sets/Relations_2_facts.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v index 7b427aa5f..7e0f8ed26 100755 --- a/theories/Sets/Relations_3.v +++ b/theories/Sets/Relations_3.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index eec50c44f..3fe27af99 100755 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (****************************************************************************) (* *) (* Naive Set Theory in Coq *) diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 5d9162fdb..b18b5634a 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index d29262427..a4e2bedfd 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index 260a539c7..b104152f5 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v index 068d4903a..e0c5dc914 100644 --- a/theories/Wellfounded/Inverse_Image.v +++ b/theories/Wellfounded/Inverse_Image.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index 7b78ddb9c..6a4ac7652 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index a6da918e3..a51b876ab 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index a97cadc27..b89e6c15b 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index e58e002a4..697313f0a 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index e2da52b53..12f65b44e 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Wellfounded/Wellfounded.v b/theories/Wellfounded/Wellfounded.v index a30007e27..696a9ea0c 100644 --- a/theories/Wellfounded/Wellfounded.v +++ b/theories/Wellfounded/Wellfounded.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Zarith/Wf_Z.v b/theories/Zarith/Wf_Z.v index 6910717b4..eab0874c0 100644 --- a/theories/Zarith/Wf_Z.v +++ b/theories/Zarith/Wf_Z.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Zarith/ZArith.v b/theories/Zarith/ZArith.v index 4bdcca1c5..b9b572137 100644 --- a/theories/Zarith/ZArith.v +++ b/theories/Zarith/ZArith.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/theories/Zarith/ZArith_dec.v b/theories/Zarith/ZArith_dec.v index 403c95fad..ee7ee48b7 100644 --- a/theories/Zarith/ZArith_dec.v +++ b/theories/Zarith/ZArith_dec.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/theories/Zarith/Zmisc.v b/theories/Zarith/Zmisc.v index bc90b0612..663fe535c 100644 --- a/theories/Zarith/Zmisc.v +++ b/theories/Zarith/Zmisc.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/theories/Zarith/Zsyntax.v b/theories/Zarith/Zsyntax.v index 9be0d8ed5..adc1fb64b 100644 --- a/theories/Zarith/Zsyntax.v +++ b/theories/Zarith/Zsyntax.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/theories/Zarith/auxiliary.v b/theories/Zarith/auxiliary.v index 0b69cd236..be642fa67 100644 --- a/theories/Zarith/auxiliary.v +++ b/theories/Zarith/auxiliary.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (**************************************************************************) (* *) (* Binary Integers *) diff --git a/theories/Zarith/fast_integer.v b/theories/Zarith/fast_integer.v index d301a7d40..f64093034 100644 --- a/theories/Zarith/fast_integer.v +++ b/theories/Zarith/fast_integer.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/theories/Zarith/zarith_aux.v b/theories/Zarith/zarith_aux.v index 5b247589f..a9c0c9976 100644 --- a/theories/Zarith/zarith_aux.v +++ b/theories/Zarith/zarith_aux.v @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) (**************************************************************************) diff --git a/tools/coq-tex.ml b/tools/coq-tex.ml index 69882c0ce..e5355a7ae 100644 --- a/tools/coq-tex.ml +++ b/tools/coq-tex.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index c7ef3f354..52d4740ea 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 0c9407cb2..f19dafcd9 100755 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll index d12e8518f..9c4c482fb 100755 --- a/tools/coqdep_lexer.mll +++ b/tools/coqdep_lexer.mll @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) { (* $Id: *) diff --git a/tools/gallina.ml b/tools/gallina.ml index f013c5788..ea26b616d 100644 --- a/tools/gallina.ml +++ b/tools/gallina.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll index 4a7568a18..e3a81912a 100644 --- a/tools/gallina_lexer.mll +++ b/tools/gallina_lexer.mll @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/class.ml b/toplevel/class.ml index 4d8e5ba2c..2a6067565 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/class.mli b/toplevel/class.mli index f2d35aa8e..7e2b32d71 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/command.ml b/toplevel/command.ml index 49dd7b887..a5b1b3b1d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/command.mli b/toplevel/command.mli index 3b20efe07..83ce53567 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 64273724d..133029253 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index f81d88eae..81a83eeea 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 41f266514..f1cc40461 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index 53af17474..ff4e169d9 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 4d1a2e2ad..fdaf56706 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli index 7cd5aab39..2f7b247ac 100644 --- a/toplevel/discharge.mli +++ b/toplevel/discharge.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/errors.ml b/toplevel/errors.ml index 708832d30..3d1cbf1ae 100644 --- a/toplevel/errors.ml +++ b/toplevel/errors.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/errors.mli b/toplevel/errors.mli index 2fe4e9188..2207608a8 100644 --- a/toplevel/errors.mli +++ b/toplevel/errors.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml index 442735ddf..d76fba078 100644 --- a/toplevel/fhimsg.ml +++ b/toplevel/fhimsg.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli index 7823c7347..33f9f4c2b 100644 --- a/toplevel/fhimsg.mli +++ b/toplevel/fhimsg.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 2abfb6cc1..a32bcc77f 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index 57300f5c0..0c7c15eab 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/line_oriented_parser.ml b/toplevel/line_oriented_parser.ml index 780780412..04c715176 100644 --- a/toplevel/line_oriented_parser.ml +++ b/toplevel/line_oriented_parser.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/line_oriented_parser.mli b/toplevel/line_oriented_parser.mli index cfaa1a318..492afab1b 100644 --- a/toplevel/line_oriented_parser.mli +++ b/toplevel/line_oriented_parser.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index c567a2f94..163f2a16d 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index b51a9a43d..34fbbef84 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index e4b170654..148033c7f 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 8fd717ff5..b3508f85f 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index b86573c95..17c3f192f 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml index 26ca3b1cc..66a41e2c1 100644 --- a/toplevel/protectedtoplevel.ml +++ b/toplevel/protectedtoplevel.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/protectedtoplevel.mli b/toplevel/protectedtoplevel.mli index f70d1dc3d..b4efd842b 100644 --- a/toplevel/protectedtoplevel.mli +++ b/toplevel/protectedtoplevel.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/record.ml b/toplevel/record.ml index f24051fd1..5df670982 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $:Id$ *) diff --git a/toplevel/record.mli b/toplevel/record.mli index b678cc3e5..9039dfc7d 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml index a5556e6e6..2c158ba31 100755 --- a/toplevel/recordobj.ml +++ b/toplevel/recordobj.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/recordobj.mli b/toplevel/recordobj.mli index 3a16613ed..dec66afe7 100755 --- a/toplevel/recordobj.mli +++ b/toplevel/recordobj.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/searchisos.mli b/toplevel/searchisos.mli index b6d773cd0..ed1900394 100644 --- a/toplevel/searchisos.mli +++ b/toplevel/searchisos.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index ca5e27e11..52f3a7935 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli index ac807a99a..77f2ce89d 100644 --- a/toplevel/toplevel.mli +++ b/toplevel/toplevel.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index a0eb96e59..f86609cb9 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/usage.mli b/toplevel/usage.mli index c89239b6b..4322b0c9b 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 35a1eb494..eae7fdf68 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 5e9c71d19..1266cd9dd 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 02d2ce6a3..c7e09086e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index f1a93824c..6c829e5a2 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index e4595244a..a0b434b9a 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (* $Id$ *) diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index 5863ffb7b..ed068d167 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -1,3 +1,10 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) (*i $Id$ i*) |