diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/egrammar.mli | 14 | ||||
| -rw-r--r-- | parsing/extend.mli | 14 | ||||
| -rw-r--r-- | parsing/extrawit.mli | 14 | ||||
| -rw-r--r-- | parsing/g_intsyntax.mli | 14 | ||||
| -rw-r--r-- | parsing/g_natsyntax.mli | 14 | ||||
| -rw-r--r-- | parsing/g_zsyntax.mli | 14 | ||||
| -rw-r--r-- | parsing/lexer.mli | 14 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 14 | ||||
| -rw-r--r-- | parsing/ppconstr.mli | 15 | ||||
| -rw-r--r-- | parsing/pptactic.mli | 14 | ||||
| -rw-r--r-- | parsing/ppvernac.mli | 14 | ||||
| -rw-r--r-- | parsing/prettyp.mli | 14 | ||||
| -rw-r--r-- | parsing/printer.mli | 14 | ||||
| -rw-r--r-- | parsing/printmod.mli | 14 | ||||
| -rw-r--r-- | parsing/q_util.mli | 14 | ||||
| -rw-r--r-- | parsing/tactic_printer.mli | 14 | ||||
| -rw-r--r-- | parsing/tok.ml | 14 | ||||
| -rw-r--r-- | parsing/tok.mli | 14 |
18 files changed, 126 insertions, 127 deletions
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index a0004ce38..56e6b1d61 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.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 Compat open Util diff --git a/parsing/extend.mli b/parsing/extend.mli index 597ff69a5..a05952294 100644 --- a/parsing/extend.mli +++ b/parsing/extend.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 Compat diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli index b330a8e64..83b8a95ff 100644 --- a/parsing/extrawit.mli +++ b/parsing/extrawit.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 Genarg diff --git a/parsing/g_intsyntax.mli b/parsing/g_intsyntax.mli index 40e16b83c..5db25305e 100644 --- a/parsing/g_intsyntax.mli +++ b/parsing/g_intsyntax.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 *) +(************************************************************************) (*i $$ i*) diff --git a/parsing/g_natsyntax.mli b/parsing/g_natsyntax.mli index 3751f603b..8f9b3f904 100644 --- a/parsing/g_natsyntax.mli +++ b/parsing/g_natsyntax.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 *) +(************************************************************************) (** Nice syntax for naturals. *) diff --git a/parsing/g_zsyntax.mli b/parsing/g_zsyntax.mli index 29dd60f35..6e81af28c 100644 --- a/parsing/g_zsyntax.mli +++ b/parsing/g_zsyntax.mli @@ -1,9 +1,9 @@ -(*********************************************************************** - 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 *) +(************************************************************************) (** Nice syntax for integers. *) diff --git a/parsing/lexer.mli b/parsing/lexer.mli index a8ae46fec..0e8be6895 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.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/parsing/pcoq.mli b/parsing/pcoq.mli index 31adbd6c0..1436b0e18 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.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/parsing/ppconstr.mli b/parsing/ppconstr.mli index afa744a50..59c1f3af7 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -1,11 +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 Environ diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index 34a7089fe..60e3648ab 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.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 Genarg diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli index 98511f3e5..80109af1e 100644 --- a/parsing/ppvernac.mli +++ b/parsing/ppvernac.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 Genarg diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index 913ab8b43..0a4c14944 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.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/parsing/printer.mli b/parsing/printer.mli index 241650b7d..c41dabf7d 100644 --- a/parsing/printer.mli +++ b/parsing/printer.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 Names diff --git a/parsing/printmod.mli b/parsing/printmod.mli index b7926543d..d99b44728 100644 --- a/parsing/printmod.mli +++ b/parsing/printmod.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 Names diff --git a/parsing/q_util.mli b/parsing/q_util.mli index c19a0ecf5..166b00521 100644 --- a/parsing/q_util.mli +++ b/parsing/q_util.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 Compat diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli index 129f0e671..60a47b75a 100644 --- a/parsing/tactic_printer.mli +++ b/parsing/tactic_printer.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 Sign diff --git a/parsing/tok.ml b/parsing/tok.ml index 870f2d5e7..55cbdecb9 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -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 *) +(************************************************************************) (** The type of token for the Coq lexer and parser *) diff --git a/parsing/tok.mli b/parsing/tok.mli index 0e2730b17..3764ef539 100644 --- a/parsing/tok.mli +++ b/parsing/tok.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 *) +(************************************************************************) (** The type of token for the Coq lexer and parser *) |