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, 3 insertions, 3 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 437ef58fd..33826c9f1 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)