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

2 files changed, 22 insertions, 5 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index a1b07cb9f2..ee385430c8 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -42,7 +42,7 @@ type typeclass = {
   cl_props : named_context;
   
   (* The method implementaions as projections. *)
-  cl_projs : constant list;
+  cl_projs : (identifier * constant) list;
 }
 
 type typeclasses = (global_reference, typeclass) Gmap.t
@@ -144,7 +144,7 @@ let subst (_,subst,(cl,m,inst)) =
       (na, Option.smartmap do_subst b, do_subst t)))
       ctx
   in
-  let do_subst_projs projs = list_smartmap do_subst_con projs in
+  let do_subst_projs projs = list_smartmap (fun (x, y) -> (x, do_subst_con y)) projs in
   let subst_class k cl classes = 
     let k = do_subst_gr k in
     let cl' = { cl with cl_impl = k;
@@ -175,7 +175,7 @@ let discharge (_,(cl,m,inst)) =
   let subst_class cl = 
     { cl with cl_impl = Lib.discharge_global cl.cl_impl;
       cl_context = list_smartmap discharge_named cl.cl_context;
-      cl_projs = list_smartmap Lib.discharge_con cl.cl_projs }
+      cl_projs = list_smartmap (fun (x, y) -> x, Lib.discharge_con y) cl.cl_projs }
   in
   let classes = Gmap.map subst_class cl in
   let subst_inst insts =
@@ -219,7 +219,7 @@ let update () =
 
 let add_class c = 
   classes := Gmap.add c.cl_impl c !classes;
-  methods := List.fold_left (fun acc x -> Gmap.add x c.cl_impl acc) !methods c.cl_projs;
+  methods := List.fold_left (fun acc x -> Gmap.add (snd x) c.cl_impl acc) !methods c.cl_projs;
   update ()
     
 let class_info c = 
@@ -306,6 +306,20 @@ let method_typeclass ref =
 let is_class gr = 
   Gmap.fold (fun k v acc -> acc || v.cl_impl = gr) !classes false
   
+let is_method c =
+  Gmap.mem c !methods
+
+let is_instance = function
+  | ConstRef c ->
+      (match Decls.constant_kind c with
+      | IsDefinition Instance -> true
+      | _ -> false)
+  | VarRef v ->
+      (match Decls.variable_kind v with
+      | IsDefinition Instance -> true
+      | _ -> false)
+  | _ -> false
+
 let is_implicit_arg k = 
   match k with
       ImplicitArg (ref, (n, id)) -> true
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 43ae592d5c..e3c780402f 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -38,7 +38,7 @@ type typeclass = {
   cl_props : named_context;
 
   (* The methods implementations of the typeclass as projections. *)
-  cl_projs : constant list;
+  cl_projs : (identifier * constant) list;
 }
 
 type instance
@@ -60,6 +60,9 @@ val is_class : global_reference -> bool
 val class_of_constr : constr -> typeclass option
 val dest_class_app : constr -> typeclass * constr array (* raises a UserError if not a class *)
 
+val is_instance : global_reference -> bool
+val is_method : constant -> bool
+
 (* Returns the term and type for the given instance of the parameters and fields
    of the type class. *)
 val instance_constructor : typeclass -> constr list -> constr * types