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 /pretyping | |
| 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 'pretyping')
33 files changed, 231 insertions, 0 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 2689772ce1..3e530b6720 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 310842b6d9..acd9f3089f 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 15a50bcc4e..4611008161 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 08e067f5ae..778eebff76 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 630a8bb310..4cd71d09d1 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 4ccf02b1f5..fc0cc1de22 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 bd25f93518..5f8e90cb29 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 e636f2fbd9..f7ea9352b7 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 ab6104f960..877dca8c94 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 6d19c624aa..f68c0356f5 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 82746d287e..7a1423c3c9 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 f1a247b452..9b45a50943 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 d7df2507cd..c34e07baca 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 772841e138..53f4cb9e32 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 41cf5561e7..a71fdf0be9 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 b83019b451..01ccd27fa3 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 0bce54e741..e687e5cbc4 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 985b7975c3..f35b1b10b6 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 ba8c0e4e77..717191aa8b 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 806a84d665..0e2974b0bb 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 d28732941d..f0bc559aef 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 f6fc0dbd6c..e7b5bd5efe 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 18845d8b1a..18e3b1a1f4 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 6db3545ce2..c8c43a2459 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 097eb25b8a..25e024a6cf 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 657f3d1e02..43e0a91f92 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 5eee11d19c..2e32601d9f 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 1e63907a49..6a171d7c46 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 cbe1ba7e5c..1a884300c9 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 d942a66114..f651766020 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 df3a0b9736..4d248983fa 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 afdaf58237..c39197af73 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 8fae1cd416..29cf0da627 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*) |