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

1 files changed, 2 insertions, 2 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 3b32cfd47..6b6b4871c 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