Imported Upstream version 8.4dfsgupstream/8.4dfsg

30 files changed, 238 insertions, 78 deletions

diff --git a/tools/compat5.ml b/tools/compat5.ml
index 641d80d8..663f8d44 100644
--- a/tools/compat5.ml
+++ b/tools/compat5.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/compat5.mlp b/tools/compat5.mlp
index e7e1aeef..aabf7288 100644
--- a/tools/compat5.mlp
+++ b/tools/compat5.mlp
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/compat5b.ml b/tools/compat5b.ml
index f757a065..2f104da7 100644
--- a/tools/compat5b.ml
+++ b/tools/compat5b.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/compat5b.mlp b/tools/compat5b.mlp
index cf8e5494..f7e08115 100644
--- a/tools/compat5b.mlp
+++ b/tools/compat5b.mlp
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 20117ca6..eedbf422 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -201,7 +201,7 @@ let install_doc some_vfiles some_mlifiles (_,inc_r) =
 	       if some_mlifiles then install_one_kind "mlihtml" rt;
 	   end else begin
 	     prerr_string "Warning: -R options don't have a correct common prefix,
- install-doc will put anything in $INSTALLDEFAULTROOT";
+ install-doc will put anything in $INSTALLDEFAULTROOT\n";
 	   if some_vfiles then install_one_kind "html" "$(INSTALLDEFAULTROOT)";
 	   if some_mlifiles then install_one_kind "mlihtml" "$(INSTALLDEFAULTROOT)";
 	   end in
@@ -428,7 +428,7 @@ let include_dirs (inc_i,inc_r) =
     if !some_ml4file || !some_mlfile || !some_mlifile then begin
       print "OCAMLLIBS?="; print_list "\\\n  " str_i; print "\n";
     end;
-    if !some_vfile then begin
+    if !some_vfile || !some_mllibfile || !some_mlpackfile then begin
       print "COQLIBS?="; print_list "\\\n  " str_i'; print " "; print_list "\\\n  " str_r; print "\n";
       print "COQDOCLIBS?=";   print_list "\\\n  " str_r; print "\n\n";
     end
diff --git a/tools/coq_tex.ml4 b/tools/coq_tex.ml4
index 485162ee..1a9b9c73 100644
--- a/tools/coq_tex.ml4
+++ b/tools/coq_tex.ml4
@@ -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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index bc840d2d..90cdd12d 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 2834af81..19aba41d 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index e412bc8f..c929e559 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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 53c3ba17..afc171cb 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli
index 6b6e0da9..7cea9743 100644
--- a/tools/coqdep_lexer.mli
+++ b/tools/coqdep_lexer.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-2012     *)
 (*   \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 159c6d3c..f59d6a0f 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index e2bc457e..8802c0ef 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
index 45836086..792b71fc 100644
--- a/tools/coqdoc/alpha.mli
+++ b/tools/coqdoc/alpha.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 6b8a3f5e..f37db46b 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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli
index cb511c16..adc49ed4 100644
--- a/tools/coqdoc/cpretty.mli
+++ b/tools/coqdoc/cpretty.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 925f5258..d7b54fd0 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -77,8 +77,17 @@
   let in_proof = ref None
   let in_emph = ref false
 
-  let start_emph () = in_emph := true; Output.start_emph ()
-  let stop_emph () = if !in_emph then (Output.stop_emph (); in_emph := false)
+  let in_env start stop = 
+    let r = ref false in
+    let start_env () = r := true; start () in
+    let stop_env () = if !r then stop (); r := false in
+      (fun x -> !r), start_env, stop_env
+      
+  let in_emph, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph
+  let in_quote, start_quote, stop_quote = in_env Output.start_quote Output.stop_quote
+
+  let url_buffer = Buffer.create 40
+  let url_name_buffer = Buffer.create 40
 
   let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos;
     lexbuf.lex_curr_p <- lexbuf.lex_start_p
@@ -254,7 +263,7 @@
     let nbsp,isp = count_spaces s in
     Output.indentation nbsp;
     let s = String.sub s isp (String.length s - isp) in
-    Output.ident s (lexeme_start lexbuf + isp)
+    Output.keyword s (lexeme_start lexbuf + isp)
 
 }
 
@@ -369,13 +378,17 @@ let commands =
   | "Drop"
   | "ProtectedLoop"
   | "Quit"
+  | "Restart"
   | "Load"
   | "Add"
   | "Remove" space+ "Loadpath"
   | "Print"
   | "Inspect"
   | "About"
+  | "SearchAbout"
+  | "SearchRewrite"
   | "Search"
+  | "Locate"
   | "Eval"
   | "Reset"
   | "Check"
@@ -403,6 +416,14 @@ let prog_kw =
   | "Obligations"
   | "Solve"
 
+let hint_kw = 
+  "Extern" | "Rewrite" | "Resolve" | "Immediate" | "Transparent" | "Opaque" | "Unfold" | "Constructors"
+
+let set_kw =
+    "Printing" space+ ("Coercions" | "Universes" | "All")
+  | "Implicit" space+ "Arguments"
+  
+
 let gallina_kw_to_hide =
     "Implicit" space+ "Arguments"
   | "Ltac"
@@ -410,15 +431,16 @@ let gallina_kw_to_hide =
   | "Import"
   | "Export"
   | "Load"
-  | "Hint"
+  | "Hint" space+ hint_kw
   | "Open"
   | "Close"
   | "Delimit"
   | "Transparent"
   | "Opaque"
   | ("Declare" space+ ("Morphism" | "Step") )
-  | ("Set" | "Unset") space+ "Printing" space+ "Coercions"
+  | ("Set" | "Unset") space+ set_kw
   | "Declare" space+ ("Left" | "Right") space+ "Step"
+  | "Debug" space+ ("On" | "Off")
 
 
 let section = "*" | "**" | "***" | "****"
@@ -689,7 +711,7 @@ and doc_bol = parse
   | space* nl+
       { Output.paragraph (); doc_bol lexbuf }
   | "<<" space*
-      { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
+      { Output.start_verbatim false; verbatim false lexbuf; doc_bol lexbuf }
   | eof
       { true }
   | '_'
@@ -713,8 +735,8 @@ and doc_list_bol indents = parse
             backtrack lexbuf; doc_bol lexbuf
       }
   | "<<" space*
-      { Output.start_verbatim ();
-        verbatim lexbuf;
+      { Output.start_verbatim false;
+        verbatim false lexbuf;
         doc_list_bol indents lexbuf }
   | "[[" nl
       { formatted := true;
@@ -813,6 +835,7 @@ and doc indents = parse
       { inf_rules indents lexbuf }
   | "[]"
       { Output.proofbox (); doc indents lexbuf }
+  | "{{" { url lexbuf; doc indents lexbuf }
   | "["
       { if !Cdglobals.plain_comments then Output.char '['
         else (brackets := 1;  Output.start_inline_coq (); escaped_coq lexbuf;
@@ -872,6 +895,15 @@ and doc indents = parse
       { if !Cdglobals.plain_comments then Output.char '_' else stop_emph () ;
         Output.char (lexeme_char lexbuf 1);
         doc indents lexbuf }
+  | "<<" space*
+      { Output.start_verbatim true; verbatim true lexbuf; doc_bol lexbuf }
+  | '"'
+      { if !Cdglobals.plain_comments 
+	then Output.char '"' 
+	else if in_quote ()
+	then stop_quote () 
+	else start_quote ();
+        doc indents lexbuf }
   | eof
       { false }
   | _
@@ -898,11 +930,22 @@ and escaped_html = parse
   | eof { () }
   | _   { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
 
-and verbatim = parse
-  | nl ">>" space* nl { Output.verbatim_char '\n'; Output.stop_verbatim () }
-  | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () }
-  | eof { Output.stop_verbatim () }
-  | _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
+and verbatim inline = parse
+  | nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
+  | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
+  | ">>" { Output.stop_verbatim inline }
+  | eof { Output.stop_verbatim inline }
+  | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf }
+
+and url = parse
+  | "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer }
+  | "}" { url_name lexbuf }
+  | _ { Buffer.add_char url_buffer (lexeme_char lexbuf 0); url lexbuf }
+
+and url_name = parse
+  | "}" { Output.url (Buffer.contents url_buffer) (Some (Buffer.contents url_name_buffer));
+	  Buffer.clear url_buffer; Buffer.clear url_name_buffer }
+  | _ { Buffer.add_char url_name_buffer (lexeme_char lexbuf 0); url_name lexbuf }
 
 (*s Coq, inside quotations *)
 
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index f19433e9..d319ce72 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -359,7 +359,16 @@ let read_glob vfile f =
 		Scanf.sscanf s "R%d:%d %s %s %s %s"
 		  (fun loc1 loc2 lib_dp sp id ty ->
 		    for loc=loc1 to loc2 do
-		      add_ref !cur_mod loc lib_dp sp id (type_of_string ty)
+		      add_ref !cur_mod loc lib_dp sp id (type_of_string ty);
+
+                      (* Also add an entry for each module mentioned in [lib_dp],
+                       * to use in interpolation. *)
+                      ignore (List.fold_right (fun thisPiece priorPieces ->
+                                                let newPieces = match priorPieces with
+                                                                | "" -> thisPiece
+                                                                | _ -> thisPiece ^ "." ^ priorPieces in
+                                                add_ref !cur_mod loc "" "" newPieces Library;
+                                                newPieces) (Str.split (Str.regexp_string ".") lib_dp) "")
 		    done)
 	       with _ -> ())
 	  | _ ->
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index bb775d26..8c658a90 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index b1303f18..b33ec1f0 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 3aed28b4..cd33528a 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -31,21 +31,25 @@ let is_keyword =
   build_table
     [ "About"; "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "Compute"; "CoFixpoint";
       "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example";
-      "Export"; "Fact"; "Fix"; "Fixpoint"; "Function"; "Generalizable"; "Global"; "Grammar"; "Goal"; "Hint";
+      "Export"; "Fact"; "Fix"; "Fixpoint"; "Function"; "Generalizable"; "Global"; "Grammar";
+      "Guarded"; "Goal"; "Hint"; "Debug"; "On";
       "Hypothesis"; "Hypotheses";
-      "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive";
+      "Resolve"; "Unfold"; "Immediate"; "Extern"; "Constructors"; "Rewrite";
+      "Implicit"; "Import"; "Inductive";
       "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
       "Module"; "Module Type"; "Declare Module"; "Include";
-      "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "Proof"; "Proof with"; "Qed";
-      "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
+      "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed";
+      "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes";
       "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
+      "Search"; "SearchAbout"; "SearchRewrite";
       "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
       "Notation"; "Reserved Notation"; "Tactic Notation";
       "Delimit"; "Bind"; "Open"; "Scope"; "Inline";
       "Implicit Arguments"; "Add"; "Strict";
       "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
-      "subgoal"; "vm_compute";
-      "Opaque"; "Transparent";
+      "subgoal"; "subgoals"; "vm_compute";
+      "Opaque"; "Transparent"; "Time";
+      "Extraction"; "Extract";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
@@ -53,14 +57,20 @@ let is_keyword =
       (*i (* coq terms *) *)
       "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "fun";
       "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
+      "fix"; "cofix";
       (* Ltac *)
-      "before"; "after"
+      "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta";
+      (* Notations *)
+      "level"; "associativity"; "no"
        ]
 
 let is_tactic =
   build_table
     [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
-      "elimtype"; "progress"; "setoid_rewrite";
+      "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; 
+      "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct";
+      "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate";
+      "quote"; "eexact"; "autorewrite";
       "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
       "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
       "set"; "assert"; "do"; "repeat";
@@ -69,8 +79,10 @@ let is_tactic =
       "reflexivity"; "symmetry"; "transitivity";
       "replace"; "setoid_replace"; "inversion"; "inversion_clear";
       "pattern"; "intuition"; "congruence"; "fail"; "fresh";
-      "trivial"; "exact"; "tauto"; "firstorder"; "ring";
-      "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto" ]
+      "trivial"; "tauto"; "firstorder"; "ring";
+      "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; "eauto";
+      "change"; "fold"; "hnf"; "lazy"; "simple"; "eexists"; "debug"; "idtac"; "first"; "type of"; "pose";
+      "eval"; "instantiate"; "until" ]
 
 (*s Current Coq module *)
 
@@ -261,6 +273,12 @@ module Latex = struct
 	| '^' | '~' as c ->
 	    Buffer.add_char buff '\\'; Buffer.add_char buff c;
 	    Buffer.add_string buff "{}"
+        | '\'' ->
+            if i < String.length s - 1 && s.[i+1] = '\'' then begin
+              Buffer.add_char buff '\''; Buffer.add_char buff '{';
+              Buffer.add_char buff '}'
+            end else
+              Buffer.add_char buff '\''
 	| c ->
 	    Buffer.add_char buff c
       done;
@@ -282,9 +300,23 @@ module Latex = struct
 
   let stop_latex_math () = output_char '$'
 
-  let start_verbatim () = printf "\\begin{verbatim}"
+  let start_quote () = output_char '`'; output_char '`'
+  let stop_quote () = output_char '\''; output_char '\''
+    
+  let start_verbatim inline = 
+    if inline then printf "\\texttt{"
+    else printf "\\begin{verbatim}"
 
-  let stop_verbatim () = printf "\\end{verbatim}\n"
+  let stop_verbatim inline =
+    if inline then printf "}"
+    else printf "\\end{verbatim}\n"
+
+  let url addr name = 
+    printf "%s\\footnote{\\url{%s}}"
+      (match name with
+       | None -> ""
+       | Some n -> n)
+      addr
 
   let indentation n =
     if n == 0 then
@@ -342,11 +374,19 @@ module Latex = struct
     | Some ref -> reference s ref
     | None -> if issymbchar then output_string s else printf "\\coqdocvar{%s}" s
 
+  let last_was_in = ref false
+
   let sublexer c loc =
-    let tag =
-      try Some (Index.find (get_module false) loc) with Not_found -> None
-    in
-    Tokens.output_tagged_symbol_char tag c
+    if c = '*' && !last_was_in then begin
+      Tokens.flush_sublexer ();
+      output_char '*'
+    end else begin
+      let tag =
+        try Some (Index.find (get_module false) loc) with Not_found -> None
+      in
+      Tokens.output_tagged_symbol_char tag c
+    end;
+    last_was_in := false
 
   let initialize () =
     Tokens.token_tree := token_tree_latex;
@@ -357,7 +397,11 @@ module Latex = struct
   let translate s =
     match Tokens.translate s with Some s -> s | None -> escaped s
 
+  let keyword s loc = 
+    printf "\\coqdockw{%s}" (translate s)
+
   let ident s loc =
+    last_was_in := s = "in";
     try
       let tag = Index.find (get_module false) loc in
       reference (translate s) tag
@@ -559,8 +603,22 @@ module Html = struct
   let start_latex_math () = ()
   let stop_latex_math () = ()
 
-  let start_verbatim () = printf "<pre>"
-  let stop_verbatim () = printf "</pre>\n"
+  let start_quote () = char '"'
+  let stop_quote () = start_quote ()
+
+  let start_verbatim inline = 
+    if inline then printf "<tt>"
+    else printf "<pre>"
+
+  let stop_verbatim inline = 
+    if inline then printf "</tt>" 
+    else printf "</pre>\n"
+
+  let url addr name = 
+    printf "<a href=\"%s\">%s</a>" addr 
+      (match name with
+       | Some n -> n
+       | None -> addr)
 
   let module_ref m s =
     match find_module m with
@@ -615,6 +673,9 @@ module Html = struct
   let translate s =
     match Tokens.translate s with Some s -> s | None -> escaped s
 
+  let keyword s loc = 
+    printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
+
   let ident s loc =
     if is_keyword s then begin
       printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
@@ -915,19 +976,28 @@ module TeXmacs = struct
 
   let stop_latex_math () = output_char '>'
 
-  let start_verbatim () = in_doc := true; printf "<\\verbatim>"
+  let start_verbatim inline = in_doc := true; printf "<\\verbatim>"
+  let stop_verbatim inline = in_doc := false; printf "</verbatim>"
 
-  let stop_verbatim () = in_doc := false; printf "</verbatim>"
+  let url addr name = 
+    printf "%s<\\footnote><\\url>%s</url></footnote>" addr
+      (match name with
+       | None -> ""
+       | Some n -> n)
+
+  let start_quote () = output_char '`'; output_char '`'
+  let stop_quote () = output_char '\''; output_char '\''
 
   let indentation n = ()
 
+  let keyword s =
+    printf "<kw|"; raw_ident s; printf ">"
+
   let ident_true s =
-    if is_keyword s then begin
-      printf "<kw|"; raw_ident s; printf ">"
-    end else begin
-      raw_ident s
-    end
+    if is_keyword s then keyword s
+    else raw_ident s
 
+  let keyword s loc = keyword s
   let ident s _ = if !in_doc then ident_true s else raw_ident s
 
   let output_sublexer_string doescape issymbchar tag s =
@@ -1042,13 +1112,21 @@ module Raw = struct
   let start_latex_math () = ()
   let stop_latex_math () = ()
 
-  let start_verbatim () = ()
+  let start_verbatim inline = ()
+  let stop_verbatim inline = ()
+
+  let url addr name = 
+    match name with
+    | Some n -> printf "%s (%s)" n addr
+    | None -> printf "%s" addr
 
-  let stop_verbatim () = ()
+  let start_quote () = printf "\""
+  let stop_quote () = printf "\""
 
   let indentation n =
       for i = 1 to n do printf " " done
 
+  let keyword s loc = raw_ident s
   let ident s loc = raw_ident s
 
   let sublexer c l = char c
@@ -1162,6 +1240,7 @@ let rule = select Latex.rule Html.rule TeXmacs.rule Raw.rule
 
 let nbsp = select Latex.nbsp Html.nbsp TeXmacs.nbsp Raw.nbsp
 let char = select Latex.char Html.char TeXmacs.char Raw.char
+let keyword = select Latex.keyword Html.keyword TeXmacs.keyword Raw.keyword
 let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident
 let sublexer = select Latex.sublexer Html.sublexer TeXmacs.sublexer Raw.sublexer
 let initialize = select Latex.initialize Html.initialize TeXmacs.initialize Raw.initialize
@@ -1189,12 +1268,20 @@ let start_verbatim =
   select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim Raw.start_verbatim
 let stop_verbatim =
   select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim
-let verbatim_char =
-  select output_char Html.char TeXmacs.char Raw.char
+let verbatim_char inline =
+  select (if inline then Latex.char else output_char) Html.char TeXmacs.char Raw.char
 let hard_verbatim_char = output_char
 
+let url = 
+  select Latex.url Html.url TeXmacs.url Raw.url
+
+let start_quote =
+  select Latex.start_quote Html.start_quote TeXmacs.start_quote Raw.start_quote
+let stop_quote =
+  select Latex.stop_quote Html.stop_quote TeXmacs.stop_quote Raw.stop_quote
+
 let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions = 
-  start_verbatim ();
+  start_verbatim false;
   let dumb_line = 
        function (sp,ln) -> (String.iter char ((String.make sp ' ') ^ ln);
                             char '\n')
@@ -1204,7 +1291,7 @@ let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions =
                                 | Some s -> " " ^ s 
                                 | None -> ""));
      List.iter dumb_line conclusions);
-  stop_verbatim ()
+  stop_verbatim false
 
 let inf_rule = select inf_rule_dumb Html.inf_rule inf_rule_dumb inf_rule_dumb
 
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 53d88666..80f39011 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -60,6 +60,7 @@ val rule : unit -> unit
 
 val nbsp : unit -> unit
 val char : char -> unit
+val keyword : string -> loc -> unit
 val ident : string -> loc -> unit
 val sublexer : char -> loc -> unit
 val initialize : unit -> unit
@@ -70,13 +71,17 @@ val latex_char : char -> unit
 val latex_string : string -> unit
 val html_char : char -> unit
 val html_string : string -> unit
-val verbatim_char : char -> unit
+val verbatim_char : bool -> char -> unit
 val hard_verbatim_char : char -> unit
 
 val start_latex_math : unit -> unit
 val stop_latex_math : unit -> unit
-val start_verbatim : unit -> unit
-val stop_verbatim : unit -> unit
+val start_verbatim : bool -> unit
+val stop_verbatim : bool -> unit
+val start_quote : unit -> unit
+val stop_quote : unit -> unit
+
+val url : string -> string option -> unit
 
 (* this outputs an inference rule in one go.  You pass it the list of
    assumptions, then the middle line info, then the conclusion (which
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
index a228797e..10a105f9 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-2012     *)
 (*   \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..e9c74307 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-2012     *)
 (*   \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 9d254684..a5376ec4 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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/escape_string.ml b/tools/escape_string.ml
new file mode 100644
index 00000000..50e8faad
--- /dev/null
+++ b/tools/escape_string.ml
@@ -0,0 +1 @@
+print_string (String.escaped Sys.argv.(1))
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index f2255981..1e889639 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/gallina.ml b/tools/gallina.ml
index 3d7b1a2c..7b051d1c 100644
--- a/tools/gallina.ml
+++ b/tools/gallina.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index b7a42cb6..cfbfac98 100644
--- a/tools/gallina_lexer.mll
+++ b/tools/gallina_lexer.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/mingwpath.ml b/tools/mingwpath.ml
new file mode 100644
index 00000000..f01b62cc
--- /dev/null
+++ b/tools/mingwpath.ml
@@ -0,0 +1,15 @@
+(** Mingwpath *)
+
+(** Converts mingw-encoded filenames such as:
+
+      /c/Program Files/Ocaml/bin
+
+    to a more windows-friendly form (but still with / instead of \) :
+
+      c:/Program Files/Ocaml/bin
+
+    This nice hack was suggested by Benjamin Monate (cf bug #2526)
+    to mimic the cygwin-specific tool cygpath
+*)
+
+print_string Sys.argv.(1)