diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-24 15:57:30 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-24 15:57:30 +0000 |
commit | 8d99bfcdc0915c006bffba6d5ffe14c683b9eb65 (patch) | |
tree | f66bf6b10fae56354ae82f811c2a8273d5d30e13 /ide | |
parent | 27882e4edd07e306333fdc024330982741416a19 (diff) |
Updated all headers for 8.3 and trunk
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
-rw-r--r-- | ide/command_windows.ml | 2 | ||||
-rw-r--r-- | ide/command_windows.mli | 2 | ||||
-rw-r--r-- | ide/config_lexer.mll | 2 | ||||
-rw-r--r-- | ide/config_parser.mly | 6 | ||||
-rw-r--r-- | ide/coq.ml | 2 | ||||
-rw-r--r-- | ide/coq.mli | 2 | ||||
-rw-r--r-- | ide/coq_commands.ml | 2 | ||||
-rw-r--r-- | ide/coq_lex.mll | 2 | ||||
-rw-r--r-- | ide/coq_tactics.ml | 2 | ||||
-rw-r--r-- | ide/coq_tactics.mli | 2 | ||||
-rw-r--r-- | ide/coqide.ml | 3 | ||||
-rw-r--r-- | ide/coqide.mli | 2 | ||||
-rw-r--r-- | ide/gtk_parsing.ml | 2 | ||||
-rw-r--r-- | ide/highlight.mll | 2 | ||||
-rw-r--r-- | ide/ideproof.ml | 2 | ||||
-rw-r--r-- | ide/ideutils.ml | 2 | ||||
-rw-r--r-- | ide/ideutils.mli | 2 | ||||
-rw-r--r-- | ide/preferences.ml | 2 | ||||
-rw-r--r-- | ide/preferences.mli | 2 | ||||
-rw-r--r-- | ide/tags.ml | 3 | ||||
-rw-r--r-- | ide/typed_notebook.ml | 2 | ||||
-rw-r--r-- | ide/uim/coqide-rules.scm | 2 | ||||
-rw-r--r-- | ide/undo.ml | 2 | ||||
-rw-r--r-- | ide/undo_lablgtk_ge212.mli | 2 | ||||
-rw-r--r-- | ide/undo_lablgtk_ge26.mli | 2 | ||||
-rw-r--r-- | ide/undo_lablgtk_lt26.mli | 2 | ||||
-rw-r--r-- | ide/utf8_convert.mll | 2 |
27 files changed, 29 insertions, 31 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index fbad08812..0d0cdfc2e 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/command_windows.mli b/ide/command_windows.mli index 29b734b37..9a073d38f 100644 --- a/ide/command_windows.mli +++ b/ide/command_windows.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index cafa96e43..8d9ede078 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/config_parser.mly b/ide/config_parser.mly index 104d31f3c..8c414d388 100644 --- a/ide/config_parser.mly +++ b/ide/config_parser.mly @@ -1,10 +1,10 @@ -/***********************************************************************) +/************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************/ +(************************************************************************/ %{ diff --git a/ide/coq.ml b/ide/coq.ml index 92ded059c..78b1060ed 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/coq.mli b/ide/coq.mli index 4b59b5e75..8554a7757 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 1d56489df..623b334e0 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index 01c3025e6..406d152cd 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/coq_tactics.ml b/ide/coq_tactics.ml index 307ee2522..7a865d5e2 100644 --- a/ide/coq_tactics.ml +++ b/ide/coq_tactics.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/coq_tactics.mli b/ide/coq_tactics.mli index 41219fdf6..498a1bbc6 100644 --- a/ide/coq_tactics.mli +++ b/ide/coq_tactics.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/coqide.ml b/ide/coqide.ml index 7e742b55d..54e130731 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1,7 +1,6 @@ - (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/coqide.mli b/ide/coqide.mli index f91ce0184..3522bee44 100644 --- a/ide/coqide.mli +++ b/ide/coqide.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index 5411499ca..bb2bebe51 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/highlight.mll b/ide/highlight.mll index 0a623ca38..2ed5737b0 100644 --- a/ide/highlight.mll +++ b/ide/highlight.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/ideproof.ml b/ide/ideproof.ml index e8f21e239..e77996a8f 100644 --- a/ide/ideproof.ml +++ b/ide/ideproof.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 46e6d43eb..0d1704e72 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 993856a3a..f15cd120c 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/preferences.ml b/ide/preferences.ml index b8eb07cc5..a99424cf7 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/preferences.mli b/ide/preferences.mli index cd955d7bd..41a581d57 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/tags.ml b/ide/tags.ml index 3b407a19d..52ba54dcb 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -1,7 +1,6 @@ - (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/typed_notebook.ml b/ide/typed_notebook.ml index 1438a9333..048cc6e24 100644 --- a/ide/typed_notebook.ml +++ b/ide/typed_notebook.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/uim/coqide-rules.scm b/ide/uim/coqide-rules.scm index e41889c1b..4e32a9655 100644 --- a/ide/uim/coqide-rules.scm +++ b/ide/uim/coqide-rules.scm @@ -1,6 +1,6 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; v ; The Coq Proof Assistant / The Coq Development Team ;; -;; <O___,, ; CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud ;; +;; <O___,, ; INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 ;; ;; \VV/ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; // ; This file is distributed under the terms of the ;; ;; ; GNU Lesser General Public License Version 2.1 ;; diff --git a/ide/undo.ml b/ide/undo.ml index 56b8196bb..1b6beeb24 100644 --- a/ide/undo.ml +++ b/ide/undo.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/undo_lablgtk_ge212.mli b/ide/undo_lablgtk_ge212.mli index c0280702d..d9451fd1a 100644 --- a/ide/undo_lablgtk_ge212.mli +++ b/ide/undo_lablgtk_ge212.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/undo_lablgtk_ge26.mli b/ide/undo_lablgtk_ge26.mli index ab51a66b2..a2eb65bd1 100644 --- a/ide/undo_lablgtk_ge26.mli +++ b/ide/undo_lablgtk_ge26.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/undo_lablgtk_lt26.mli b/ide/undo_lablgtk_lt26.mli index 330accc7b..b193007b6 100644 --- a/ide/undo_lablgtk_lt26.mli +++ b/ide/undo_lablgtk_lt26.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll index b1eb0f4c2..d29ae0bd5 100644 --- a/ide/utf8_convert.mll +++ b/ide/utf8_convert.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |