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/toplevel/record.ml b/toplevel/record.ml
index f6815d537..83332e823 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -131,7 +131,7 @@ let instantiate_possibly_recursive_type indsp paramdecls fields =
   substl_rel_context (subst@[mkInd indsp]) fields
 
 (* We build projections *)
-let declare_projections indsp ?name coers fields =
+let declare_projections indsp ?(kind=StructureComponent) ?name coers fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
   let paramdecls = mib.mind_params_ctxt in
@@ -172,7 +172,7 @@ let declare_projections indsp ?name coers fields =
                     const_entry_type = Some projtyp;
                     const_entry_opaque = false;
 		    const_entry_boxed = Flags.boxed_definitions() } in
-		  let k = (DefinitionEntry cie,IsDefinition StructureComponent) in
+		  let k = (DefinitionEntry cie,IsDefinition kind) in
 		  let kn = declare_internal_constant fid k in
 		  Flags.if_verbose message (string_of_id fid ^" is defined");
 		  kn