diff options
| author | herbelin | 2010-06-22 06:31:30 +0000 |
|---|---|---|
| committer | herbelin | 2010-06-22 06:31:30 +0000 |
| commit | d6c87f235a98c05a26b4a0e87129335d034219af (patch) | |
| tree | 0cdbf9db7dc808621befc220892b9b7e083cdfe0 /library | |
| parent | a1f06f016be512c21cb475491ec9924eea7ff288 (diff) | |
New script dev/tools/change-header to automatically update Coq files headers.
Applied it to fix mli file headers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/decl_kinds.mli | 14 | ||||
| -rw-r--r-- | library/declare.mli | 14 | ||||
| -rw-r--r-- | library/declaremods.mli | 14 | ||||
| -rw-r--r-- | library/decls.mli | 14 | ||||
| -rw-r--r-- | library/dischargedhypsmap.mli | 14 | ||||
| -rw-r--r-- | library/global.mli | 14 | ||||
| -rw-r--r-- | library/goptions.mli | 14 | ||||
| -rw-r--r-- | library/heads.mli | 14 | ||||
| -rw-r--r-- | library/impargs.mli | 14 | ||||
| -rw-r--r-- | library/lib.mli | 14 | ||||
| -rw-r--r-- | library/libnames.mli | 14 | ||||
| -rw-r--r-- | library/libobject.mli | 14 | ||||
| -rw-r--r-- | library/library.mli | 14 | ||||
| -rw-r--r-- | library/nameops.mli | 14 | ||||
| -rw-r--r--[-rwxr-xr-x] | library/nametab.mli | 14 | ||||
| -rw-r--r-- | library/states.mli | 14 | ||||
| -rw-r--r-- | library/summary.mli | 14 |
17 files changed, 119 insertions, 119 deletions
diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli index 2c04d0fdd7..bdf01bfc01 100644 --- a/library/decl_kinds.mli +++ b/library/decl_kinds.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) open Util open Libnames diff --git a/library/declare.mli b/library/declare.mli index db9e1aa6d2..3ff91cc5e7 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) open Names open Libnames diff --git a/library/declaremods.mli b/library/declaremods.mli index b7126147e4..de12c036cc 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) open Util open Names diff --git a/library/decls.mli b/library/decls.mli index 34a96cd8b7..641038d555 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) open Names open Sign diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli index 98e3d93d54..8284e68a20 100644 --- a/library/dischargedhypsmap.mli +++ b/library/dischargedhypsmap.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) open Libnames open Term diff --git a/library/global.mli b/library/global.mli index d29aca5d33..97024a40bd 100644 --- a/library/global.mli +++ b/library/global.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) open Names open Univ diff --git a/library/goptions.mli b/library/goptions.mli index c63845ae08..72a16c0263 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) (** This module manages customization parameters at the vernacular level *) diff --git a/library/heads.mli b/library/heads.mli index 5a0df84237..4598a21ea2 100644 --- a/library/heads.mli +++ b/library/heads.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) open Names open Term diff --git a/library/impargs.mli b/library/impargs.mli index 2eab1af668..74c33dc045 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) open Names open Libnames diff --git a/library/lib.mli b/library/lib.mli index 5fb65a41ff..9a0a0ddafe 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) (** Lib: record of operations, backtrack, low-level sections *) diff --git a/library/libnames.mli b/library/libnames.mli index 4e9ddcb561..d4f70fde0c 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) open Pp open Util diff --git a/library/libobject.mli b/library/libobject.mli index 87bbbe89d6..471416df06 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) open Names open Libnames diff --git a/library/library.mli b/library/library.mli index 87e376ab9b..7fc613aa0c 100644 --- a/library/library.mli +++ b/library/library.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) open Util open Names diff --git a/library/nameops.mli b/library/nameops.mli index 121f0ce776..13e01306bf 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) open Names diff --git a/library/nametab.mli b/library/nametab.mli index 2f81ff50e1..9019e27abb 100755..100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) open Util open Pp diff --git a/library/states.mli b/library/states.mli index 9b5872bde6..bacc9fb768 100644 --- a/library/states.mli +++ b/library/states.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) (** {6 States of the system} *) diff --git a/library/summary.mli b/library/summary.mli index 0f6aaddaf7..0ef3b6f30f 100644 --- a/library/summary.mli +++ b/library/summary.mli @@ -1,10 +1,10 @@ -(*********************************************************************** - v * The Coq Proof Assistant / The Coq Development Team - <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud - \VV/ ************************************************************* - // * This file is distributed under the terms of the - * GNU Lesser General Public License Version 2.1 - ***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) (** This module registers the declaration of global tables, which will be kept in synchronization during the various backtracks of the system. *) |