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

8 files changed, 79 insertions, 25 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 89bf68bb8..333a26f03 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -117,7 +117,7 @@ open Topconstr
 
 let declare_implicit_proj c proj imps sub =
   let len = List.length c.cl_context in
-  let (ctx, _) = decompose_prod_n (len + 1) (Typeops.type_of_constant (Global.env()) proj) in
+  let (ctx, _) = decompose_prod_n (len + 1) (Typeops.type_of_constant (Global.env()) (snd proj)) in
   let expls =
     let rec aux i expls = function
 	[] -> expls
@@ -130,8 +130,8 @@ let declare_implicit_proj c proj imps sub =
   in 
   let expls = expls @ List.map (function (ExplByPos (i, n), f) -> (ExplByPos (succ len + i, n)), f | _ -> assert(false)) imps in
     if sub then 
-      declare_instance_cst true proj;
-    Impargs.declare_manual_implicits true (ConstRef proj) true expls
+      declare_instance_cst true (snd proj);
+    Impargs.declare_manual_implicits true (ConstRef (snd proj)) true expls
       
 let declare_implicits impls subs cl =
   Util.list_iter3 (fun p imps sub -> declare_implicit_proj cl p imps sub)
@@ -186,7 +186,7 @@ let declare_structure env id idbuild params arity fields =
   let kn = Command.declare_mutual_with_eliminations true mie [] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let id = Nameops.next_ident_away id (ids_of_context (Global.env())) in
-  let kinds,sp_projs = Record.declare_projections rsp ~name:id (List.map (fun _ -> false) fields) fields in
+  let kinds,sp_projs = Record.declare_projections rsp ~kind:Method ~name:id (List.map (fun _ -> false) fields) fields in
   let _build = ConstructRef (rsp,1) in
     Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
     rsp
@@ -314,11 +314,12 @@ let new_class id par ar sup props =
 	    let proj_cst = Declare.declare_constant proj_name
 	      (DefinitionEntry proj_entry, IsDefinition Definition) 
 	    in
-	      ConstRef cst, [proj_cst]
+	      ConstRef cst, [proj_name, proj_cst]
 	| _ ->
 	    let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
 	    let kn = declare_structure env0 (snd id) idb params arity fields in
-	      IndRef kn, (List.map Option.get (Recordops.lookup_projections kn))
+	      IndRef kn, (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y)
+			     fields (Recordops.lookup_projections kn))
   in
   let ctx_context =
     List.map (fun ((na, b, t) as d) -> 
@@ -546,8 +547,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
 	      List.fold_left
 		(fun (props, rest) (id,_,_) -> 
 		  try 
-		    let (_, c) = List.find (fun ((_,id'), c) -> id' = id) rest in
+		    let ((loc, mid), c) = List.find (fun ((_,id'), c) -> id' = id) rest in
 		    let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
+		      Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
 		      c :: props, rest'
 		  with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
 		([], props) k.cl_props
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index bbb7b85ca..88147b539 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -28,7 +28,8 @@ type binder_def_list = (identifier located * identifier located list * constr_ex
  
 val binders_of_lidents : identifier located list -> local_binder list
 
-val declare_implicit_proj : typeclass -> constant -> Impargs.manual_explicitation list -> bool -> unit
+val declare_implicit_proj : typeclass -> (identifier * constant) -> 
+  Impargs.manual_explicitation list -> bool -> unit
 (*
 val infer_super_instances : env -> constr list ->
   named_context -> named_context -> types list * identifier list * named_context
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7be01c666..11b849c4f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -144,6 +144,7 @@ let declare_global_definition ident ce local imps =
 
 let declare_definition_hook = ref ignore
 let set_declare_definition_hook = (:=) declare_definition_hook
+let get_declare_definition_hook () = !declare_definition_hook
 
 let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
   let imps, ce = constant_entry_of_com (bl,c,typopt,false,boxed) in
@@ -871,13 +872,13 @@ let interp_recursive fixkind l boxed =
 
 let build_recursive l b =
   let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
-  let fixl = List.map (fun ((id,_,bl,typ,def),ntn) -> 
+  let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) -> 
     ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn))
     l in
   interp_recursive (IsFixpoint g) fixl b
 
 let build_corecursive l b =
-  let fixl = List.map (fun ((id,bl,typ,def),ntn) -> 
+  let fixl = List.map (fun (((_,id),bl,typ,def),ntn) -> 
     ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn))
     l in
   interp_recursive IsCoFixpoint fixl b
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 8448817f6..595057616 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -30,6 +30,7 @@ open Redexpr
    functions of [Declare]; they return an absolute reference to the
    defined object *)
 
+val get_declare_definition_hook : unit -> (Entries.definition_entry -> unit)
 val set_declare_definition_hook : (Entries.definition_entry -> unit) -> unit
 
 val definition_message : identifier -> unit
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
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 5ba8b04e1..c2c6b72ee 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -21,7 +21,7 @@ open Topconstr
    as coercions accordingly to [coers]; it returns the absolute names of projections *)
 
 val declare_projections :
-  inductive -> ?name:identifier -> bool list -> rel_context -> bool list * constant option list
+  inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier -> bool list -> rel_context -> bool list * constant option list
 
 val definition_structure :
   lident with_coercion * local_binder list *
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 49690256c..30d993256 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -300,7 +300,20 @@ let start_proof_and_print k l hook =
   print_subgoals ();
   if !pcoq <> None then (Option.get !pcoq).start_proof ()
 
+let dump_definition (loc, id) s =
+  Flags.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) (string_of_id id))
+
+let dump_variable (loc, id) s = ()
+(*   Flags.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) *)
+(* 			(string_of_kn (Lib.make_kn id))) *)
+
+let dump_constraint ty ((loc, n), _, _) =
+  match n with
+    | Name id -> dump_definition (loc, id) ty
+    | Anonymous -> ()
+
 let vernac_definition (local,_,_ as k) (_,id as lid) def hook =
+  if !Flags.dump then dump_definition lid "def";
   match def with
   | ProveBody (bl,t) ->   (* local binders, typ *)
       if Lib.is_modtype () then
@@ -319,6 +332,11 @@ let vernac_definition (local,_,_ as k) (_,id as lid) def hook =
       declare_definition id k bl red_option c typ_opt hook
 
 let vernac_start_proof kind l lettop hook =
+  if !Flags.dump then
+    List.iter (fun (id, _) -> 
+      match id with
+      | Some lid -> dump_definition lid "prf"
+      | None -> ()) l;
   if not(refining ()) then
     if lettop then
       errorlabstrm "Vernacentries.StartProof"
@@ -351,13 +369,29 @@ let vernac_exact_proof c =
 	(str "Command 'Proof ...' can only be used at the beginning of the proof")
   	
 let vernac_assumption kind l nl=
-  List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c false false nl) l
-
-let vernac_inductive f indl = build_mutual indl f
-
-let vernac_fixpoint = build_recursive
-
-let vernac_cofixpoint = build_corecursive
+  let global = fst kind = Global in
+  List.iter (fun (is_coe,(idl,c)) -> 
+    if !dump then
+      List.iter (fun lid -> if global then dump_definition lid "ax" else
+	  dump_variable lid "var") idl;
+    declare_assumption idl is_coe kind [] c false false nl) l
+
+let vernac_inductive f indl = 
+  if !dump then
+    List.iter (fun ((lid, _, _, cstrs), _) ->
+      dump_definition lid "ind";
+      List.iter (fun (_, (lid, _)) ->
+	dump_definition lid "constr") cstrs)
+      indl;
+  build_mutual indl f
+
+let vernac_fixpoint l b = 
+  List.iter (fun ((lid, _, _, _, _), _) -> dump_definition lid "def") l;
+  build_recursive l b
+
+let vernac_cofixpoint l b =
+  List.iter (fun ((lid, _, _, _), _) -> dump_definition lid "def") l;
+  build_corecursive l b
 
 let vernac_scheme = build_scheme
 
@@ -487,7 +521,8 @@ let vernac_include = function
 let vernac_record struc binders sort nameopt cfs =
   let const = match nameopt with 
     | None -> add_prefix "Build_" (snd (snd struc))
-    | Some (_,id) -> id in
+    | Some (_,id as lid) ->
+	if !dump then dump_definition lid "constr"; id in
   let sigma = Evd.empty in
   let env = Global.env() in
   let s = interp_constr sigma env sort in
@@ -496,7 +531,13 @@ let vernac_record struc binders sort nameopt cfs =
     | Sort s -> s
     | _ -> user_err_loc
         (constr_loc sort,"definition_structure", str "Sort expected") in
-  ignore(Record.definition_structure (struc,binders,cfs,const,s))
+    if !dump then (
+      dump_definition (snd struc) "rec";
+      List.iter (fun (_, x) ->
+	match x with
+	| AssumExpr ((loc, Name id), _) -> dump_definition (loc,id) "proj"
+	| _ -> ()) cfs);
+    ignore(Record.definition_structure (struc,binders,cfs,const,s))
 
   (* Sections *)
 
@@ -537,15 +578,21 @@ let vernac_identity_coercion stre id qids qidt =
 
 (* Type classes *)
 let vernac_class id par ar sup props =
+  if !dump then (
+    dump_definition id "class";
+    List.iter (fun (lid, _, _) -> dump_definition lid "meth") props);
   Classes.new_class id par ar sup props
-
+ 
 let vernac_instance glob sup inst props pri =
+  if !dump then dump_constraint "inst" inst;
   ignore(Classes.new_instance ~global:glob sup inst props pri)
 
 let vernac_context l =
+  if !dump then List.iter (dump_constraint "var") l;
   Classes.context l
 
 let vernac_declare_instance id =
+  if !dump then dump_definition id "inst";
   Classes.declare_instance false id
 
 (***********)
@@ -679,7 +726,9 @@ let vernac_declare_tactic_definition = Tacinterp.add_tacdef
 
 let vernac_hints = Auto.add_hints
 
-let vernac_syntactic_definition = Command.syntax_definition 
+let vernac_syntactic_definition lid =
+  dump_definition lid "syndef";
+  Command.syntax_definition (snd lid)
 
 let vernac_declare_implicits local r = function
   | Some imps ->
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index cce6f9a62..8f54e699e 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -288,7 +288,7 @@ type vernac_expr =
   | VernacDeclareTacticDefinition of
       rec_flag * (reference * bool * raw_tactic_expr) list
   | VernacHints of locality_flag * lstring list * hints
-  | VernacSyntacticDefinition of identifier * (identifier list * constr_expr) *
+  | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) *
       locality_flag * onlyparsing_flag
   | VernacDeclareImplicits of locality_flag * lreference * 
       (explicitation * bool * bool) list option