diff options
| -rw-r--r-- | COPYRIGHT | 43 | ||||
| -rw-r--r-- | dev/header | 2 | ||||
| -rwxr-xr-x | dev/tools/change-header | 37 |
3 files changed, 42 insertions, 40 deletions
@@ -1,35 +1,14 @@ -The Coq proof assistant V7 and V8 includes software developed by the -Coq development team inside the LogiCal project, at INRIA, CNRS and -University Paris Sud. + The Coq proof assistant -Copyright 1999-2004 The Coq development team, -INRIA-CNRS, University Paris Sud, All rights reserved. - -This version contains modifications by Lionel Elie Mamane -<lionel@mamane.lu> done while under employment of the Radboud -University Nijmegen. However, no copyright-assignment-to-employer -agreement was signed, and copyright of articles and books written on -work time rest with the employee. By analogy, it is Lionel's opinion -that copyright on these changes rests with him. +Copyright 1999-2010 The Coq development team, INRIA, CNRS, University +Paris Sud, University Paris 7, Ecole Polytechnique. This product includes also software developed by - Yves Bertot, Lemme, INRIA Sophia-Antipolis (plugins/interface, -parsing/search.ml) - Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega) - Pierre Courtieu, Lemme (plugins/funind) - Loïc Pottier, Lemme, INRIA Sophia-Antipolis (plugins/fourier) - Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml) - -The file CREDITS contains a list of past contributors -The credits section in Reference Manual introduction details -contributions. - -The Coq development Team (march 2004) - Bruno Barras (INRIA) - Pierre Corbineau (Université Paris Sud) - Jean-Christophe Filliâtre (CNRS) - Hugo Herbelin (INRIA) - Pierre Letouzey (Université Paris Sud) - Claude Marché (Université Paris Sud-INRIA) - Christine Paulin (Université Paris Sud) - Clément Renard (INRIA) + Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega) + Pierre Courtieu and Julien Forest, CNAM (plugins/funind) + Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml) + Pierre Corbineau, Radbout University, Nijmegen (declarative mode) + John Harrison, University of Cambridge (csdp wrapper) + +The file CREDITS contains a list of contributors. +The credits section in the Reference Manual details contributions. diff --git a/dev/header b/dev/header index 57945e47e..d90be792d 100644 --- a/dev/header +++ b/dev/header @@ -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/dev/tools/change-header b/dev/tools/change-header index 8b3560e89..61cc86660 100755 --- a/dev/tools/change-header +++ b/dev/tools/change-header @@ -16,17 +16,40 @@ if [ ! -f $newheader ]; then echo Cannot read file $newheader; exit 1; fi n=`wc -l $oldheader | sed -e "s/ *\([0-9]*\).*/\1/g"` nsucc=`expr $n + 1` -filter="-name \*.mli -o -name \*.ml -o -name \*.ml4 -o -name \*.mll -o -name \*.mly" +linea='(* -*- coding:utf-8 -*- *)' +lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)' -for i in `find . $filter`; do - head -n +$n $i > $i.head.tmp$$ +modified=0 +kept=0 + +for i in `find . -name \*.mli -o -name \*.ml -o -name \*.ml4 -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do + headline=`head -n 1 $i` + if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then + # Has emacs header + head -n +$nsucc $i | tail -n $n > $i.head.tmp$$ + hasheadline=1 + nnext=`expr $nsucc + 1` + else + head -n +$n $i > $i.head.tmp$$ + hasheadline=0 + nnext=$nsucc + fi if diff -a -q $oldheader $i.head.tmp$$ > /dev/null; then - rm $i.head.tmp$$ echo "$i: header changed" - cat dev/header > $i.tmp$$ - tail -n +$nsucc $i >> $i.tmp$$ + if [ $hasheadline = 1 ]; then + echo $headline > $i.tmp$$ + else + touch $i.tmp$$ + fi + cat $newheader >> $i.tmp$$ + tail -n +$nnext $i >> $i.tmp$$ mv $i.tmp$$ $i + modified=`expr $modified + 1` else - echo "$i: old header not found, file untouched" + kept=`expr $kept + 1` fi + rm $i.head.tmp$$ done + +echo $modified files updated +echo $kept files unchanged |