Imported Upstream version 8.3.pl3upstream/8.3.pl3

12 files changed, 55 insertions, 34 deletions

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        *)