Improvements on coqdoc by adding more information into .glob

files, about definitions and type of references.
- Add missing location information on fixpoints/cofixpoint in topconstr and
syntactic definitions in vernacentries for correct dumping.
- Dump definition information in vernacentries: defs, constructors,
projections etc...
- Modify coqdoc/index.mll to use this information instead of trying to
scan the file.
- Use the type information in latex output, update coqdoc.sty accordingly.
- Use the hyperref package to do crossrefs between definition and 
  references to coq objects in latex.  

Next step is to test and debug it on bigger developments.

On the side:
- Fix Program Let which was adding a Global definition. 
- Correct implicits for well-founded Program Fixpoints.
- Add new [Method] declaration kind.


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

4 files changed, 10 insertions, 10 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 3b32cfd471..6b6b4871cf 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -55,7 +55,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) =
   let ty = match tyc with
       Some ty -> ty
     | None -> CHole (loc, None) in
-  (snd id,(n,ro),bl,ty,body)
+  (id,(n,ro),bl,ty,body)
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
   let _ = Option.map (fun (aloc,_) ->
@@ -65,7 +65,7 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
   let ty = match tyc with
       Some ty -> ty
     | None -> CHole (loc, None) in
-  (snd id,bl,ty,body)
+  (id,bl,ty,body)
 
 let mk_fix(loc,kw,id,dcls) =
   if kw then 
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 437ef58fdb..33826c9f18 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -258,7 +258,7 @@ GEXTEND Gram
   ;
   (* (co)-fixpoints *)
   rec_definition:
-    [ [ id = ident; 
+    [ [ id = identref; 
 	bl = binders_let_fixannot;
         ty = type_cstr; 
 	":="; def = lconstr; ntn = decl_notation ->
@@ -282,7 +282,7 @@ GEXTEND Gram
 	  ((id,(ni,snd annot),bl,ty,def),ntn) ] ]
   ;
   corec_definition:
-    [ [ id = ident; bl = binders_let; ty = type_cstr; ":=";
+    [ [ id = identref; bl = binders_let; ty = type_cstr; ":=";
         def = lconstr; ntn = decl_notation ->
           ((id,bl,ty,def),ntn) ] ]
   ;
@@ -808,7 +808,7 @@ GEXTEND Gram
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
          VernacInfix (local,(op,modl),p,sc)
-     | IDENT "Notation"; local = locality; id = ident; idl = LIST0 ident; 
+     | IDENT "Notation"; local = locality; id = identref; idl = LIST0 ident; 
 	 ":="; c = constr;
 	 b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] ->
            VernacSyntacticDefinition (id,(idl,c),local,b)
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 44aabc2cb4..0f0c38adc1 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -393,7 +393,7 @@ let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
   pr_opt_type_spc pr t ++ str " :=" ++
   pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c
 
-let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) =
+let pr_fixdecl pr prd dangling_with_for ((_,id),(n,ro),bl,t,c) =
   let annot =
     match ro with
 	CStructRec ->
@@ -407,7 +407,7 @@ let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) =
   in
     pr_recursive_decl pr prd dangling_with_for id bl annot t c
 
-let pr_cofixdecl pr prd dangling_with_for (id,bl,t,c) =
+let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) =
   pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c
 
 let pr_recursive pr_decl id = function
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index c31defe094..c4b5c2d3e8 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -584,7 +584,7 @@ let rec pr_vernac = function
         | LocalRawAssum (nal,_,_) -> nal
         | LocalRawDef (_,_) -> [] in
       let pr_onerec = function
-        | (id,(n,ro),bl,type_,def),ntn ->
+        | ((loc,id),(n,ro),bl,type_,def),ntn ->
             let (bl',def,type_) =
               if Flags.do_translate() then extract_def_binders def type_
               else ([],def,type_) in
@@ -616,7 +616,7 @@ let rec pr_vernac = function
         prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs)
 
   | VernacCoFixpoint (corecs,b) ->
-      let pr_onecorec ((id,bl,c,def),ntn) =
+      let pr_onecorec (((loc,id),bl,c,def),ntn) =
         let (bl',def,c) =
               if Flags.do_translate() then extract_def_binders def c
               else ([],def,c) in
@@ -815,7 +815,7 @@ let rec pr_vernac = function
       pr_hints local dbnames h pr_constr pr_pattern_expr
   | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) ->
       hov 2
-        (str"Notation " ++ pr_locality local ++ pr_id id ++ 
+        (str"Notation " ++ pr_locality local ++ pr_lident id ++ 
 	 prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++
          pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
   | VernacDeclareImplicits (local,q,None) ->