Imported Upstream version 8.3.pl3upstream/8.3.pl3

22 files changed, 76 insertions, 55 deletions

diff --git a/tools/beautify-archive b/tools/beautify-archive
index aac6f3e0..ccfeb3db 100644
--- a/tools/beautify-archive
+++ b/tools/beautify-archive
@@ -47,6 +47,6 @@ for i in $vfiles; do
   mv -u -f $NEWARCHIVE/$i $i
 done
 echo -------- Beautification completed -------------------------------------
-echo Old files are in directory '"$OLDARCHIVE"'
+echo Old files are in directory '"'$OLDARCHIVE'"'
 echo New files are in current directory
-echo You can now remove the beautification directory '"$NEWARCHIVE"'
+echo You can now remove the beautification directory '"'$NEWARCHIVE'"'
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index e4a3d5a4..50f0344b 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_makefile.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: coq_makefile.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (* créer un Makefile pour un développement Coq automatiquement *)
 
@@ -334,7 +334,7 @@ let rec special = function
 let custom sps =
   let pr_path (file,dependencies,com) =
     print file; print ": "; print dependencies; print "\n";
-    print "\t"; print com; print "\n\n"
+    if com <> "" then (print "\t"; print com); print "\n\n"
   in
     if sps <> [] then section "Custom targets.";
     List.iter pr_path sps
@@ -570,7 +570,7 @@ let check_overlapping_include (inc_i,inc_r) =
     | [] -> ()
     | (pdir,_,abspdir)::l ->
 	if not (is_prefix pwd abspdir) then
-	  Printf.eprintf "Warning: in option -R, %s is not a subdirectoty of the current directory\n" pdir;
+	  Printf.eprintf "Warning: in option -R, %s is not a subdirectory of the current directory\n" pdir;
 	List.iter (fun (pdir',_,abspdir') ->
 	  if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then
 	    Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l;
diff --git a/tools/coq_tex.ml4 b/tools/coq_tex.ml4
index 647e6d7e..14a37a2e 100644
--- a/tools/coq_tex.ml4
+++ b/tools/coq_tex.ml4
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coq_tex.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: coq_tex.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (* coq-tex
  * JCF, 16/1/98
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 3093fa6c..d36fdae3 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqdep.ml 13983 2011-04-08 17:57:56Z herbelin $ *)
+(* $Id: coqdep.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Printf
 open Coqdep_lexer
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index d50d1604..68197e0c 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqdep_boot.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: coqdep_boot.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Coqdep_common
 
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 851b7089..5d06b888 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 3a2bc4d3..28ea4200 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coqdep_lexer.mll 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: coqdep_lexer.mll 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 {
 
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index 664ead9a..83bfa5ed 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: alpha.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: alpha.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Cdglobals
 
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
index 00b3d11b..ec5b084f 100644
--- a/tools/coqdoc/alpha.mli
+++ b/tools/coqdoc/alpha.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: alpha.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: alpha.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (* Alphabetic order. *)
 
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 63ea264b..5cb670dc 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -49,6 +49,22 @@ type glob_source_t =
 
 let glob_source = ref DotGlob
 
+(** A weaker analog of the function in Envars *)
+
+let guess_coqlib () =
+  let file = "states/initial.coq" in
+  if Sys.file_exists (Filename.concat Coq_config.coqlib file)
+  then Coq_config.coqlib
+  else
+    let coqbin = Filename.dirname Sys.executable_name in
+    let prefix = Filename.dirname coqbin in
+    let rpath = if Coq_config.local then [] else
+	(if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
+    let coqlib = List.fold_left Filename.concat prefix rpath in
+    if Sys.file_exists (Filename.concat coqlib file) then coqlib
+    else
+      Coq_config.coqlib
+
 let header_trailer = ref true
 let header_file = ref ""
 let header_file_spec = ref false
@@ -66,7 +82,7 @@ let page_title = ref ""
 let title = ref ""
 let externals = ref true
 let coqlib = ref Coq_config.wwwstdlib
-let coqlib_path = ref Coq_config.coqlib
+let coqlib_path = ref (guess_coqlib ())
 let raw_comments = ref false
 let parse_comments = ref false
 let plain_comments = ref false
diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli
index 2a0a9091..085ae122 100644
--- a/tools/coqdoc/cpretty.mli
+++ b/tools/coqdoc/cpretty.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cpretty.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: cpretty.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Index
 
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 177058b3..63850bd5 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -1,13 +1,13 @@
 (* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cpretty.mll 13692 2010-12-06 23:55:10Z herbelin $ i*)
+(*i $Id: cpretty.mll 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*s Utility functions for the scanners *)
 
@@ -279,7 +279,7 @@ let firstchar =
   (* '\206' ([ '\145' - '\183'] | '\187') | *)
   (* '\xCF' [ '\x00' - '\xCE' ] |  *)
   (* utf-8 letterlike symbols *)
-  '\206' ('\160' | [ '\177'-'\183'] | '\187') |
+  '\206' (['\145'-'\161'] | ['\163'-'\187']) |
   '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
     | '\129' [ '\176'-'\187' ] (* superscripts *)
     | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
@@ -902,7 +902,9 @@ and escaped_coq = parse
   | eof
       { Tokens.flush_sublexer () }
   | (identifier '.')* identifier
-      { Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
+      { Tokens.flush_sublexer();
+        Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
+        escaped_coq lexbuf }
   | space
       { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0);
         escaped_coq lexbuf }
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index a28e1197..a2cb995e 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -1,13 +1,13 @@
 (* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.ml 13676 2010-12-04 10:34:21Z herbelin $ i*)
+(*i $Id: index.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Filename
 open Lexing
@@ -61,8 +61,10 @@ let full_ident sp id =
   then id
   else ""
 
-let add_def loc ty sp id =
-  Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty));
+let add_def loc1 loc2 ty sp id =
+  for loc = loc1 to loc2 do
+    Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty))
+  done;
   Hashtbl.add deftable id (Ref (!current_library, full_ident sp id, ty))
 
 let add_ref m loc m' sp id ty =
@@ -341,16 +343,16 @@ let read_glob f =
 		    for loc=loc1 to loc2 do
 		      add_ref !cur_mod loc lib_dp sp id (type_of_string ty)
 		    done)
-	       with _ ->
-	       try
-		Scanf.sscanf s "R%d %s %s %s %s"
-		  (fun loc lib_dp sp id ty ->
-		    add_ref !cur_mod loc lib_dp sp id (type_of_string ty))
 	       with _ -> ())
 	  | _ ->
-	      try Scanf.sscanf s "%s %d %s %s"
-		(fun ty loc sp id -> add_def loc (type_of_string ty) sp id)
+	      try Scanf.sscanf s "not %d %s %s"
+		(fun loc sp id -> add_def loc loc (type_of_string "not") sp id)
+	      with Scanf.Scan_failure _ ->
+	      try Scanf.sscanf s "%s %d:%d %s %s"
+		(fun ty loc1 loc2 sp id ->
+                  add_def loc1 loc2 (type_of_string ty) sp id)
 	      with Scanf.Scan_failure _ -> ()
+
       end
     done; assert false
   with End_of_file ->
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 72cd7a9f..a009e9dc 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: index.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Cdglobals
 
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 06d57f5e..23dadbc1 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -1,13 +1,13 @@
 (* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: main.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: main.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
  *  - handling of absolute filenames (function coq_module)
@@ -135,7 +135,7 @@ let add_path dir name =
 
 (* turn A/B/C into A.B.C *)
 let rec name_of_path p name dirname suffix =
-  if p = dirname then String.concat "." (name::suffix)
+  if p = dirname then String.concat "." (if name = "" then suffix else (name::suffix))
   else
     let subdir = Filename.dirname dirname in
     if subdir = dirname then raise Not_found
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 4f9dd169..eefcfd11 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -1,13 +1,13 @@
 (* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.ml 13676 2010-12-04 10:34:21Z herbelin $ i*)
+(*i $Id: output.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Cdglobals
 open Index
@@ -49,6 +49,7 @@ let is_keyword =
       "Implicit Arguments"; "Add"; "Strict";
       "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
       "subgoal";
+      "Opaque"; "Transparent";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index dd37c6ad..dcd9072d 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: output.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Cdglobals
 open Index
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
index a228797e..9de39083 100644
--- a/tools/coqdoc/tokens.ml
+++ b/tools/coqdoc/tokens.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli
index 6adc2d8c..3b756e18 100644
--- a/tools/coqdoc/tokens.mli
+++ b/tools/coqdoc/tokens.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index f95a553a..380448be 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,7 +9,7 @@
 (* coqwc - counts the lines of spec, proof and comments in Coq sources
  * Copyright (C) 2003 Jean-Christophe Filliâtre *)
 
-(*i $Id: coqwc.mll 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: coqwc.mll 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*s {\bf coqwc.} Counts the lines of spec, proof and comments in a Coq source.
     It assumes the files to be lexically well-formed. *)
diff --git a/tools/gallina.ml b/tools/gallina.ml
index a7b7d344..161d86a8 100644
--- a/tools/gallina.ml
+++ b/tools/gallina.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: gallina.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: gallina.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Gallina_lexer
 
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index d025b8c0..638d5936 100644
--- a/tools/gallina_lexer.mll
+++ b/tools/gallina_lexer.mll
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: gallina_lexer.mll 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: gallina_lexer.mll 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 {
  open Lexing