diff options
| author | filliatr | 2001-03-15 13:38:59 +0000 |
|---|---|---|
| committer | filliatr | 2001-03-15 13:38:59 +0000 |
| commit | 187dc15532f0c6f380d7bcb07adc2180c29fedc2 (patch) | |
| tree | d7bacf01519ca82b5745d2c493c7f7f1826106af /contrib | |
| parent | 23741168b109daece8bb588b9c5fb4506e7726ce (diff) | |
entetes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
35 files changed, 245 insertions, 0 deletions
diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v index 9e0f23c2d0..0f9668756c 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 2b4c66da6c..ab303b0947 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 066bb2a6d1..bf6940d1cc 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 a6f46235b0..6aa5b7977c 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 4c1d492c17..df5a414a1f 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 27390de44f..55d80d8467 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 1bd795c090..376b069d0d 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 525b8dc3d9..95b81fe108 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 12e39d0441..6fd5d86571 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 6e302989fe..4fdb2e9eae 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 ba7d59e724..83189ec579 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 be80e419a6..ff8dce97fe 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 2f06ad3972..2d40d97f52 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 8c646ae087..6c4a6191b5 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 af673b097d..a7f67f1815 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 c808232371..52607a4a0d 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 5d343880e0..3d29e0503f 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 824012d124..c2585b3e08 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 821c4b2021..71bfbe290a 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 86f1a2e334..6d78494a22 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 14d69e2b02..0dfb1f4e35 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 e7c995cf3b..f97c81c408 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 b6f75a5841..c94dce065e 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 6bb1f5aa9a..7626899850 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 536d2d3034..94b5093c70 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 c04eee57ec..867ab22fbe 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 a8adfe2f63..2de8611764 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 ac3af30b8d..c82ccecb00 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 0e200313c7..589c1580ea 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 5c6b788aa3..f1d91371e9 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 635e83f68a..60e16ab19b 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 0510d978da..fbdb584ee8 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 906cf8b078..3927827276 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 1c9b22070a..0ddc01c9a4 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 ffa0d5fc79..093727f2f1 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 *) |