Misc fixes.

- Correct backtracking function of coqdoc to handle the _p fields of lexers
- Try a better typesetting of [[ ]] inline code considering it as
blocks and not purely inline code like [ ] escapings.
- Rework latex macros for better factorization and support external
references in pdf output.
- Better criterion for generalization of variables in dependent
elimination tactic and better error message in [specialize_hypothesis].
- In autounfold, don't put the core unfolds by default.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12474 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 117 insertions, 99 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 93f4eedff2..dc2f8ad0aa 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -55,9 +55,13 @@ let add_generalizable gen table =
 
 let cache_generalizable_type (_,(local,cmd)) =
   generalizable_table := add_generalizable cmd !generalizable_table
+
+let load_generalizable_type _ (_,(local,cmd)) =
+  generalizable_table := add_generalizable cmd !generalizable_table
     
 let (in_generalizable, _) =
   declare_object {(default_object "GENERALIZED-IDENT") with
+    load_function = load_generalizable_type;
     cache_function = cache_generalizable_type;
     classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj)
   }
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 2fd822636e..c21185c511 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -552,7 +552,7 @@ GEXTEND Gram
       | IDENT "Generalizable"; ["Variable" | IDENT "Variables"];
            gen = [ IDENT "none" -> None | IDENT "all" -> Some [] | 
 	       idl = LIST1 identref -> Some idl ] ->
-	     VernacGeneralizable (use_section_locality (), gen) ] ]
+	     VernacGeneralizable (use_non_locality (), gen) ] ]
   ;
   implicit_name:
     [ [ "!"; id = ident -> (id, false, true)
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 17361f2e65..e89b61d46a 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -421,9 +421,9 @@ let autosimpl db cl =
 
 TACTIC EXTEND autounfold
 | [ "autounfold" hintbases(db) "in" hyp(id) ] ->
-    [ autounfold (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, InHyp)) ]
+    [ autounfold (match db with None -> ["core"] | Some x -> x) (Some (id, InHyp)) ]
 | [ "autounfold" hintbases(db) ] ->
-    [ autounfold (match db with None -> ["core"] | Some x -> "core"::x) None ]
+    [ autounfold (match db with None -> ["core"] | Some x -> x) None ]
       END
 
 let unfold_head env (ids, csts) c = 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a740d7bb2b..b9d2d9cfef 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2160,7 +2160,7 @@ let lift_together l = lift_togethern 0 l
 
 let lift_list l = List.map (lift 1) l
 
-let ids_of_constr vars c =
+let ids_of_constr ?(all=false) vars c =
   let rec aux vars c =
     match kind_of_term c with
     | Var id -> Idset.add id vars
@@ -2169,7 +2169,8 @@ let ids_of_constr vars c =
 	| Construct (ind,_)
 	| Ind ind ->
             let (mib,mip) = Global.lookup_inductive ind in
-	      array_fold_left_from mib.Declarations.mind_nparams
+	      array_fold_left_from
+		(if all then 0 else mib.Declarations.mind_nparams)
 		aux vars args
 	| _ -> fold_constr aux vars c)
     | _ -> fold_constr aux vars c
@@ -2248,6 +2249,23 @@ let hyps_of_vars env sign nogen hyps =
         sign 
     in lh
 
+exception Seen
+
+let linear vars args = 
+  let seen = ref vars in
+    try 
+      Array.iter (fun i -> 
+	let rels = ids_of_constr ~all:true Idset.empty i in
+	let seen' = 
+	  Idset.fold (fun id acc ->
+	    if Idset.mem id acc then raise Seen
+	    else Idset.add id acc)
+	    rels !seen
+	in seen := seen')
+	args;
+      true
+    with Seen -> false
+
 let abstract_args gl generalize_vars dep id = 
   let c = pf_get_hyp_typ gl id in
   let sigma = project gl in
@@ -2299,7 +2317,8 @@ let abstract_args gl generalize_vars dep id =
 	in 
 	let f', args' = decompose_indapp f args in
 	let dogen, f', args' =
-	  if not (array_distinct args) then true, f', args'
+	  let parvars = ids_of_constr ~all:true Idset.empty f' in
+	  if not (linear parvars args') then true, f, args
 	  else
 	    match array_find_i (fun i x -> not (isVar x)) args' with
 	    | None -> false, f', args'
@@ -2390,6 +2409,11 @@ let specialize_hypothesis id gl =
     else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
       
 
+let specialize_hypothesis id gl =
+  if occur_id [] id (pf_concl gl) then
+    tclFAIL 0 (str "Specialization not allowed on dependent hypotheses") gl 
+  else specialize_hypothesis id gl
+
 let dependent_pattern c gl =
   let cty = pf_type_of gl c in
   let deps =
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index b50b755f61..4314d07d6f 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -65,6 +65,25 @@
 % macro for typesetting tactic identifiers
 \newcommand{\coqdoctac}[1]{\texttt{#1}}
 
+% These are the real macros used by coqdoc, their typesetting is 
+% based on the above macros by default.
+
+\newcommand{\coqdoclibrary}[1]{\coqdoccst{#1}}
+\newcommand{\coqdocinductive}[1]{\coqdocind{#1}}
+\newcommand{\coqdocdefinition}[1]{\coqdoccst{#1}}
+\newcommand{\coqdocvariable}[1]{\coqdocvar{#1}}
+\newcommand{\coqdocconstructor}[1]{\coqdocconstr{#1}}
+\newcommand{\coqdoclemma}[1]{\coqdoccst{#1}}
+\newcommand{\coqdocclass}[1]{\coqdocind{#1}}
+\newcommand{\coqdocinstance}[1]{\coqdoccst{#1}}
+\newcommand{\coqdocmethod}[1]{\coqdoccst{#1}}
+\newcommand{\coqdocabbreviation}[1]{\coqdoccst{#1}}
+\newcommand{\coqdocrecord}[1]{\coqdocind{#1}}
+\newcommand{\coqdocprojection}[1]{\coqdoccst{#1}}
+\newcommand{\coqdocnotation}[1]{\coqdockw{#1}}
+\newcommand{\coqdocsection}[1]{\coqdoccst{#1}}
+\newcommand{\coqdocaxiom}[1]{\coqdocax{#1}}
+\newcommand{\coqdocmoduleid}[1]{\coqdocmod{#1}}
 
 % Environment encompassing code fragments
 % !!! CAUTION: This environment may have empty contents
@@ -102,12 +121,15 @@
 
   \newcommand{\coqdef}[3]{\phantomsection\hypertarget{coq:#1}{#3}}
   \newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}}
+  \newcommand{\coqexternalref}[3]{\href{#1.html\##2}{#3}}
+
   \newcommand{\identref}[2]{\hyperlink{coq:#1}{\textsf {#2}}}
   \newcommand{\coqlibrary}[3]{\cleardoublepage\phantomsection
     \hypertarget{coq:#1}{\chapter{#2\texorpdfstring{\coqdoccst}{}{#3}}}}
 \else
   \newcommand{\coqdef}[3]{#3}
   \newcommand{\coqref}[2]{#2}
+  \newcommand{\coqexternalref}[3]{#3}
   \newcommand{\texorpdfstring}[2]{#1}
   \newcommand{\identref}[2]{\textsf{#2}}
   \newcommand{\coqlibrary}[3]{\cleardoublepage\chapter{#2\coqdoccst{#3}}}
@@ -147,54 +169,4 @@
 \def\coqdoctac#1{{\color{\coqdoctaccolor}{\texttt{#1}}}}
 \fi
 
-\newcommand{\coqdefinition}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
-\newcommand{\coqdefinitionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
-
-\newcommand{\coqvariable}[2]{\coqdocvar{#2}}
-\newcommand{\coqvariableref}[2]{\coqref{#1}{\coqdocvar{#2}}}
-
-\newcommand{\coqinductive}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
-\newcommand{\coqinductiveref}[2]{\coqref{#1}{\coqdocind{#2}}}
-
-\newcommand{\coqconstructor}[2]{\coqdef{#1}{#2}{\coqdocconstr{#2}}}
-\newcommand{\coqconstructorref}[2]{\coqref{#1}{\coqdocconstr{#2}}}
-
-\newcommand{\coqlemma}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
-\newcommand{\coqlemmaref}[2]{\coqref{#1}{\coqdoccst{#2}}}
-
-\newcommand{\coqclass}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
-\newcommand{\coqclassref}[2]{\coqref{#1}{\coqdocind{#2}}}
-
-\newcommand{\coqinstance}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
-\newcommand{\coqinstanceref}[2]{\coqref{#1}{\coqdoccst{#2}}}
-
-\newcommand{\coqmethod}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
-\newcommand{\coqmethodref}[2]{\coqref{#1}{\coqdoccst{#2}}}
-
-\newcommand{\coqabbreviation}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
-\newcommand{\coqabbreviationref}[2]{\coqref{#1}{\coqdoccst{#2}}}
-
-\newcommand{\coqrecord}[2]{\coqdef{#1}{#2}{\coqdocind{#2}}}
-\newcommand{\coqrecordref}[2]{\coqref{#1}{\coqdocind{#2}}}
-
-\newcommand{\coqprojection}[2]{\coqdef{#1}{#2}{\coqdoccst{#2}}}
-\newcommand{\coqprojectionref}[2]{\coqref{#1}{\coqdoccst{#2}}}
-
-\newcommand{\coqnotationref}[2]{\coqref{#1}{\coqdockw{#2}}}
-
-\newcommand{\coqsection}[2]{\coqdef{sec:#1}{#2}{\coqdoccst{#2}}}
-\newcommand{\coqsectionref}[2]{\coqref{sec:#1}{\coqdoccst{#2}}}
-
-%\newcommand{\coqlibrary}[2]{\chapter{Library \coqdoccst{#2}}\label{coq:#1}}
-  
-%\newcommand{\coqlibraryref}[2]{\ref{coq:#1}}
-
-\newcommand{\coqlibraryref}[2]{\coqref{#1}{\coqdoccst{#2}}}
-
-\newcommand{\coqaxiom}[2]{\coqdef{#1}{#2}{\coqdocax{#2}}}
-\newcommand{\coqaxiomref}[2]{\coqref{#1}{\coqdocax{#2}}}
-
-\newcommand{\coqmodule}[2]{\coqdef{mod:#1}{#2}{\coqdocmod{#2}}}
-\newcommand{\coqmoduleref}[2]{\coqref{mod:#1}{\coqdocmod{#2}}}
-
 \endinput
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 2820b9a88f..c20449bcdc 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -70,7 +70,9 @@
   let start_emph () = in_emph := true; Output.start_emph ()
   let stop_emph () = if !in_emph then (Output.stop_emph (); in_emph := false)
     
-  let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
+  let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos;
+    lexbuf.lex_curr_p <- lexbuf.lex_start_p
+
   let backtrack_past_newline lexbuf =
     let buf = lexeme lexbuf in
     let splits = Str.bounded_split_delim (Str.regexp "['\n']") buf 2 in
@@ -435,7 +437,9 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)"
 
 rule coq_bol = parse
   | space* nl+
-      { if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light)) then Output.empty_line_of_code (); coq_bol lexbuf }
+      { if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light)) 
+        then Output.empty_line_of_code (); 
+        coq_bol lexbuf }
   | space* "(**" space_nl
       { Output.end_coq (); Output.start_doc ();
 	let eol = doc_bol lexbuf in
@@ -707,10 +711,9 @@ and doc_list_bol indents = parse
         doc_list_bol indents lexbuf }
   | "[[" nl
       { formatted := true;
-        Output.paragraph ();
-        Output.start_inline_coq ();
+        Output.start_inline_coq_block ();
         ignore(body_bol lexbuf);
-        Output.end_inline_coq ();
+        Output.end_inline_coq_block ();
         formatted := false;
         doc_list_bol indents lexbuf }
   | space* nl space* '-'
@@ -779,9 +782,9 @@ and doc indents = parse
       { if !Cdglobals.plain_comments
         then (Output.char '['; Output.char '['; doc indents lexbuf)
         else (formatted := true;
-              Output.line_break (); Output.start_inline_coq ();
+              Output.start_inline_coq_block ();
 	      let eol = body_bol lexbuf in
-	        Output.end_inline_coq (); formatted := false;
+	        Output.end_inline_coq_block (); formatted := false;
 	        if eol then
 		  match indents with
 		  | Some ls -> doc_list_bol ls lexbuf
@@ -931,9 +934,9 @@ and comment = parse
       if !Cdglobals.parse_comments then
         if !Cdglobals.plain_comments then (Output.char '['; Output.char '[')
         else (formatted := true;
-              Output.line_break (); Output.start_inline_coq ();
+              Output.start_inline_coq_block ();
               let _ = body_bol lexbuf in
-                Output.end_inline_coq (); formatted := false);
+                Output.end_inline_coq_block (); formatted := false);
       comment lexbuf}
   | "$"
       { if !Cdglobals.parse_comments then
@@ -986,7 +989,7 @@ and body_bol = parse
   | _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
 
 and body = parse
-  | nl {Output.line_break(); body_bol lexbuf}
+  | nl {Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf}
   | nl+ space* "]]" space* nl
       { if not !formatted then
           begin
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index ae35f74458..90d0d0e007 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -252,28 +252,25 @@ module Latex = struct
 
   let module_ref m s =
     printf "\\moduleid{%s}{" m; raw_ident s; printf "}"
-      (*i
-    match find_module m with
-    | Local ->
-	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    | External m when !externals ->
-	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    | External _ | Unknown ->
-	raw_ident s
-    i*)
 
   let ident_ref m fid typ s =
     let id = if fid <> "" then (m ^ "." ^ fid) else m in
     match find_module m with
-      | Local ->
-	  printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
-      | External _ when !externals ->
-	  printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
+      | Local -> 
+	  if typ = Variable then (printf "\\coqdoc%s{" (type_name typ); raw_ident s; printf "}")
+	  else
+	    (printf "\\coqref{"; label_ident id; printf "}{\\coqdoc%s{" (type_name typ);
+	     raw_ident s; printf "}}")
+      | External m when !externals ->
+	  printf "\\coqexternalref{"; label_ident m; printf "}{";
+	  label_ident fid; printf "}{\\coqdoc%s{" (type_name typ); raw_ident s; printf "}}"
       | External _ | Unknown ->
-	  printf "\\coq%sref{" (type_name typ); label_ident id; printf "}{"; raw_ident s; printf "}"
+	  (* printf "\\coqref{"; label_ident id; printf "}{" *)
+	  printf "\\coqdoc%s{" (type_name typ); raw_ident s; printf "}"
 
   let defref m id ty s =
-    printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}"
+    printf "\\coqdef{"; label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}{";
+    printf "\\coqdoc%s{" (type_name ty); raw_ident s; printf "}}"
 
   let reference s = function
     | Def (fullid,typ) ->
@@ -286,24 +283,18 @@ module Latex = struct
 	printf "\\coqdocvar{"; raw_ident s; printf "}"
 
   let ident s loc =
-    if is_keyword s then begin
-      printf "\\coqdockw{"; raw_ident s; printf "}"
-    end else begin
-      begin
-	try
-	  reference s (Index.find (get_module false) loc)
-	with Not_found ->
-	  if is_tactic s then begin
-	    printf "\\coqdoctac{"; raw_ident s; printf "}"
-	  end else begin
-	    if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
-	    then
-	      try reference s (Index.find_string (get_module false) s)
-	      with _ -> (printf "\\coqdocvar{"; raw_ident s; printf "}")
-	    else (printf "\\coqdocvar{"; raw_ident s; printf "}")
-	  end
-      end
-    end
+    try
+      reference s (Index.find (get_module false) loc)
+    with Not_found ->
+      if is_tactic s then
+	(printf "\\coqdoctac{"; raw_ident s; printf "}")
+      else if is_keyword s then
+	(printf "\\coqdockw{"; raw_ident s; printf "}")
+      else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
+      then
+	try reference s (Index.find_string (get_module false) s)
+	with _ -> (printf "\\coqdocvar{"; raw_ident s; printf "}")
+      else (printf "\\coqdocvar{"; raw_ident s; printf "}")
 
   let ident s l =
     if !in_title then (
@@ -379,6 +370,10 @@ module Latex = struct
 
   let empty_line_of_code () = printf "\\coqdocemptyline\n"
 
+  let start_inline_coq_block () = line_break (); empty_line_of_code ()
+
+  let end_inline_coq_block () = empty_line_of_code ()
+
   let start_inline_coq () = ()
 
   let end_inline_coq () = ()
@@ -591,6 +586,10 @@ module Html = struct
 
   let end_inline_coq () = printf "</span>"
 
+  let start_inline_coq_block () = line_break (); start_inline_coq ()
+
+  let end_inline_coq_block () = end_inline_coq ()
+
   let paragraph () = printf "\n<br/> <br/>\n"
 
   let section lev f =
@@ -871,6 +870,10 @@ module TeXmacs = struct
 
   let end_inline_coq () = printf "]>"
 
+  let start_inline_coq_block () = line_break (); start_inline_coq ()
+
+  let end_inline_coq_block () = end_inline_coq ()
+
   let make_multi_index () = ()
 
   let make_index () = ()
@@ -966,6 +969,9 @@ module Raw = struct
   let start_inline_coq () = ()
   let end_inline_coq () = ()
 
+  let start_inline_coq_block () = line_break (); start_inline_coq ()
+  let end_inline_coq_block () = end_inline_coq ()
+
   let make_multi_index () = ()
   let make_index () = ()
   let make_toc () = ()
@@ -1004,6 +1010,12 @@ let start_inline_coq =
 let end_inline_coq =
   select Latex.end_inline_coq Html.end_inline_coq TeXmacs.end_inline_coq Raw.end_inline_coq
 
+let start_inline_coq_block =
+  select Latex.start_inline_coq_block Html.start_inline_coq_block 
+    TeXmacs.start_inline_coq_block Raw.start_inline_coq_block
+let end_inline_coq_block =
+  select Latex.end_inline_coq_block Html.end_inline_coq_block TeXmacs.end_inline_coq_block Raw.end_inline_coq_block
+
 let indentation = select Latex.indentation Html.indentation TeXmacs.indentation Raw.indentation
 let paragraph = select Latex.paragraph Html.paragraph TeXmacs.paragraph Raw.paragraph
 let line_break = select Latex.line_break Html.line_break TeXmacs.line_break Raw.line_break
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 35f056d94c..f8a25285c5 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -44,6 +44,9 @@ val end_code : unit -> unit
 val start_inline_coq : unit -> unit
 val end_inline_coq : unit -> unit
 
+val start_inline_coq_block : unit -> unit
+val end_inline_coq_block : unit -> unit
+
 val indentation : int -> unit
 val line_break : unit -> unit
 val paragraph : unit -> unit