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

9 files changed, 81 insertions, 48 deletions

diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 06c67e60b1..3a4122b838 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -56,7 +56,8 @@ let solve_tccs_in_type env id isevars evm c typ =
     (** Make all obligations transparent so that real dependencies can be sorted out by the user *)
     let obls = Array.map (fun (id, t, l, op, d) -> (id, t, l, false, d)) obls in
       match Subtac_obligations.add_definition stmt_id c' typ obls with
-	  Subtac_obligations.Defined cst -> constant_value (Global.env()) cst
+	  Subtac_obligations.Defined cst -> constant_value (Global.env()) 
+	    (match cst with ConstRef kn -> kn | _ -> assert false)
 	| _ -> 
 	    errorlabstrm "start_proof" 
 	      (str "The statement obligations could not be resolved automatically, " ++ spc () ++
@@ -105,9 +106,24 @@ let declare_assumption env isevars idl is_coe k bl c nl =
     errorlabstrm "Command.Assumption"
 	(str "Cannot declare an assumption while in proof editing mode.")
 
-let vernac_assumption env isevars kind l nl =
-  List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c nl) l
+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_constraint ty ((loc, n), _, _) =
+  match n with
+    | Name id -> dump_definition (loc, id) ty
+    | Anonymous -> ()
 
+let dump_variable lid = ()
+
+let vernac_assumption env isevars kind l nl =
+  let global = fst kind = Global in
+    List.iter (fun (is_coe,(idl,c)) -> 
+      if !Flags.dump then
+	List.iter (fun lid -> 
+	  if global then dump_definition lid "ax" 
+	  else dump_variable lid) idl;
+      declare_assumption env isevars idl is_coe kind [] c nl) l
 
 let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
@@ -118,6 +134,7 @@ let subtac (loc, command) =
   try
   match command with
 	VernacDefinition (defkind, (_, id as lid), expr, hook) -> 
+	  dump_definition lid "def";
 	    (match expr with
 	      | ProveBody (bl, t) -> 
 		  if Lib.is_modtype () then
@@ -126,12 +143,14 @@ let subtac (loc, command) =
 		  start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) 
 		    (fun _ _ -> ())
 	      | DefineBody (bl, _, c, tycon) -> 
-		   ignore(Subtac_pretyping.subtac_proof env isevars id bl c tycon))
+		   ignore(Subtac_pretyping.subtac_proof defkind env isevars id bl c tycon))
       | VernacFixpoint (l, b) -> 
+	  List.iter (fun ((lid, _, _, _, _), _) -> dump_definition lid "fix") l;
 	  let _ = trace (str "Building fixpoint") in
 	    ignore(Subtac_command.build_recursive l b)
 
       | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) ->
+	  if !Flags.dump then dump_definition id "prf";
 	  if not(Pfedit.refining ()) then
 	    if lettop then
 	      errorlabstrm "Subtac_command.StartProof"
@@ -146,11 +165,12 @@ let subtac (loc, command) =
 	  vernac_assumption env isevars stre l nl
 
       | VernacInstance (glob, sup, is, props, pri) ->
+	  if !Flags.dump then dump_constraint "inst" is;
 	  ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
 
       | VernacCoFixpoint (l, b) ->
-	  let _ = trace (str "Building cofixpoint") in
-	    ignore(Subtac_command.build_corecursive l b)
+	  List.iter (fun ((lid, _, _, _), _) -> dump_definition lid "cofix") l;
+	  ignore(Subtac_command.build_corecursive l b)
 
       (*| VernacEndProof e -> 
 	  subtac_end_proof e*)
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 01f530d19d..3ebc3bb5c5 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -173,8 +173,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
 	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
@@ -198,12 +199,13 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
 (* 	ExplByPos (i, Some na), (true, true)) *)
 (*       1 ctx *)
 (*   in *)
-      let hook cst = 
+      let hook gr = 
+	let cst = match gr with ConstRef kn -> kn | _ -> assert false in
 	let inst = Typeclasses.new_instance k pri global cst in
-	  Impargs.declare_manual_implicits false (ConstRef cst) false imps;
+	  Impargs.declare_manual_implicits false gr false imps;
 	  Typeclasses.add_instance inst
       in
       let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in
       let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
-	ignore(Subtac_obligations.add_definition id constr typ ~kind:Instance ~hook obls);
+	ignore(Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls);
 	id
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 3b4067ce89..5bff6ad1a8 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -58,10 +58,9 @@ let interp_gen kind isevars env
                ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =
   let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars (Evd.evars_of !isevars) env c in
-(*     (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); *)
   let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in
     evar_nf isevars c'
-    
+
 let interp_constr isevars env c =
   interp_gen (OfType None) isevars env c 
 
@@ -276,11 +275,6 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
 (* 		   str "Intern body " ++ pr intern_body_lam) *)
     with _ -> ()
   in
-  let _impl = 
-    if Impargs.is_implicit_args()
-    then Impargs.compute_implicits top_env top_arity
-    else [] 
-  in
   let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in
     (* Lift to get to constant arguments *)
   let lift_cst = List.length after + 1 in
@@ -309,7 +303,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
   let evm = evars_of_term (Evd.evars_of !isevars) evm fullcoqc in
   let evm = non_instanciated_map env isevars evm in
   let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in
-    Subtac_obligations.add_definition recname evars_def evars_typ evars
+    Subtac_obligations.add_definition recname evars_def evars_typ ~implicits:impls evars
 
 let nf_evar_context isevars ctx = 
   List.map (fun (n, b, t) -> 
@@ -436,14 +430,14 @@ let out_n = function
 let build_recursive l b =
   let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
     match g, l with
-	[(n, CWfRec r)], [((id,_,bl,typ,def),ntn)] ->
+	[(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
 	  ignore(build_wellfounded (id, out_n n, bl, typ, def) r false ntn false)
 
-      | [(n, CMeasureRec r)], [((id,_,bl,typ,def),ntn)] ->
+      | [(n, CMeasureRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
 	  ignore(build_wellfounded (id, out_n n, bl, typ, def) r true ntn false)
 
       | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
-	  let fixl = List.map (fun ((id,_,bl,typ,def),ntn) -> 
+	  let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) -> 
 	    ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn)) l 
 	  in interp_recursive (Command.IsFixpoint g) fixl b
       | _, _ -> 
@@ -451,7 +445,7 @@ let build_recursive l b =
 	    (str "Well-founded fixpoints not allowed in mutually recursive blocks")
 
 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) -> 
     ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn))
     l in
   interp_recursive Command.IsCoFixpoint fixl b
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 1e6a55a0e7..cdfb40b26a 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -12,8 +12,9 @@ open Entries
 open Decl_kinds
 open Util
 open Evd
+open Declare
 
-type definition_hook = constant -> unit
+type definition_hook = global_reference -> unit
 
 let pperror cmd = Util.errorlabstrm "Program" cmd
 let error s = pperror (str s)
@@ -48,7 +49,7 @@ type program_info = {
   prg_fixkind : Command.fixpoint_kind option ;
   prg_implicits : (Topconstr.explicitation * (bool * bool)) list;
   prg_notations : notations ;
-  prg_kind : definition_object_kind;
+  prg_kind : definition_kind;
   prg_hook : definition_hook;
 }
 
@@ -161,21 +162,36 @@ let declare_definition prg =
 		  my_print_constr (Global.env()) body ++ str " : " ++ 
 		  my_print_constr (Global.env()) prg.prg_type);
      with _ -> ());
+  let (local, boxed, kind) = prg.prg_kind in
   let ce = 
     { const_entry_body = body;
       const_entry_type = Some typ;
       const_entry_opaque = false;
-      const_entry_boxed = false} 
-  in
-  let c = Declare.declare_constant 
-    prg.prg_name (DefinitionEntry ce,IsDefinition prg.prg_kind)
+      const_entry_boxed = boxed} 
   in
-  let gr = ConstRef c in
-    if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
-      Impargs.declare_manual_implicits false gr (Impargs.is_implicit_args ()) prg.prg_implicits;
-    print_message (Subtac_utils.definition_message c);
-    prg.prg_hook c;
-    c
+    (Command.get_declare_definition_hook ()) ce;
+    match local with
+    | Local when Lib.sections_are_opened () ->
+        let c =
+          SectionLocalDef(ce.const_entry_body,ce.const_entry_type,false) in
+        let _ = declare_variable prg.prg_name (Lib.cwd(),c,IsDefinition kind) in
+          print_message (Subtac_utils.definition_message prg.prg_name);
+          if Pfedit.refining () then 
+            Flags.if_verbose msg_warning 
+	      (str"Local definition " ++ Nameops.pr_id prg.prg_name ++ 
+		  str" is not visible from current goals");
+          VarRef prg.prg_name
+    | (Global|Local) ->
+	let c =
+	  Declare.declare_constant 
+	    prg.prg_name (DefinitionEntry ce,IsDefinition (pi3 prg.prg_kind))
+	in
+	let gr = ConstRef c in
+	  if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
+	    Impargs.declare_manual_implicits false gr (Impargs.is_implicit_args ()) prg.prg_implicits;
+	  print_message (Subtac_utils.definition_message prg.prg_name);
+	  prg.prg_hook gr;
+	  gr
 
 open Pp
 open Ppconstr
@@ -241,7 +257,7 @@ let declare_obligation obl body =
   let constant = Declare.declare_constant obl.obl_name 
     (DefinitionEntry ce,IsProof Property)
   in
-    print_message (Subtac_utils.definition_message constant);
+    print_message (Subtac_utils.definition_message obl.obl_name);
     { obl with obl_body = Some (mkConst constant) }
       
 let try_tactics obls = 
@@ -298,7 +314,7 @@ let update_state s =
 type progress = 
     | Remain of int 
     | Dependent
-    | Defined of constant
+    | Defined of global_reference
 	  
 let obligations_message rem =
   if rem > 0 then
@@ -328,7 +344,7 @@ let update_obls prg obls rem =
 		     from_prg := List.fold_left
 		       (fun acc x -> 
 			 ProgMap.remove x.prg_name acc) !from_prg progs;
-		    Defined kn)
+		    Defined (ConstRef kn))
 		else Dependent);
     in
       update_state (!from_prg, !default_tactic_expr);
@@ -473,7 +489,7 @@ let show_term n =
     msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++ my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ my_print_constr (Global.env ()) prg.prg_body)
 
-let add_definition n b t ?(implicits=[]) ?(kind=Definition) ?(hook=fun x -> ()) obls =
+let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?(hook=fun x -> ()) obls =
   Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
   let prg = init_prog_info n b t [] None [] obls implicits kind hook in
   let obls,_ = prg.prg_obligations in
@@ -491,7 +507,7 @@ let add_definition n b t ?(implicits=[]) ?(kind=Definition) ?(hook=fun x -> ())
 	  | Remain rem when rem < 5 -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	  | _ -> res)
 	
-let add_mutual_definitions l ?(kind=Definition) notations fixkind =
+let add_mutual_definitions l ?(kind=Global,false,Definition) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
   let upd = List.fold_left
       (fun acc (n, b, t, imps, obls) ->
diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli
index 997c2479de..6d13e3bd3a 100644
--- a/contrib/subtac/subtac_obligations.mli
+++ b/contrib/subtac/subtac_obligations.mli
@@ -1,5 +1,6 @@
 open Names
 open Util
+open Libnames
 
 type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) array
     (* ident, type, location, opaque or transparent, dependencies *)
@@ -7,7 +8,7 @@ type obligation_info = (Names.identifier * Term.types * loc * bool * Intset.t) a
 type progress = (* Resolution status of a program *)
     | Remain of int  (* n obligations remaining *)
     | Dependent (* Dependent on other definitions *)
-    | Defined of constant (* Defined as id *)
+    | Defined of global_reference (* Defined as id *)
 	
 val set_default_tactic : Tacexpr.glob_tactic_expr -> unit
 val default_tactic : unit -> Proof_type.tactic
@@ -15,11 +16,11 @@ val default_tactic : unit -> Proof_type.tactic
 val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
 val get_proofs_transparency : unit -> bool
 
-type definition_hook = constant -> unit
+type definition_hook = global_reference -> unit
 
 val add_definition : Names.identifier ->  Term.constr -> Term.types -> 
   ?implicits:(Topconstr.explicitation * (bool * bool)) list ->
-  ?kind:Decl_kinds.definition_object_kind ->
+  ?kind:Decl_kinds.definition_kind ->
   ?hook:definition_hook -> obligation_info -> progress
 
 type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
@@ -27,7 +28,7 @@ type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option)
 val add_mutual_definitions : 
   (Names.identifier * Term.constr * Term.types *
       (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> 
-  ?kind:Decl_kinds.definition_object_kind ->
+  ?kind:Decl_kinds.definition_kind ->
   notations ->
   Command.fixpoint_kind -> unit
 
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index ec5af37fe2..2118dfbdda 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -136,8 +136,8 @@ let subtac_process env isevars id bl c tycon =
 
 open Subtac_obligations
 
-let subtac_proof env isevars id bl c tycon =
+let subtac_proof kind env isevars id bl c tycon =
   let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in
   let evm = Subtac_utils.evars_of_term evm Evd.empty coqc in
   let evars, def, ty = Eterm.eterm_obligations env id !isevars evm 0 coqc coqt in
-    add_definition id def ty ~implicits:imps evars
+    add_definition id def ty ~implicits:imps ~kind:kind evars
diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli
index 4af37043fd..1d8eb25070 100644
--- a/contrib/subtac/subtac_pretyping.mli
+++ b/contrib/subtac/subtac_pretyping.mli
@@ -19,5 +19,5 @@ val interp :
 val subtac_process : env -> evar_defs ref -> identifier -> local_binder list ->
   constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list
 
-val subtac_proof : env -> evar_defs ref -> identifier -> local_binder list ->
+val subtac_proof : Decl_kinds.definition_kind -> env -> evar_defs ref -> identifier -> local_binder list ->
   constr_expr -> constr_expr option -> Subtac_obligations.progress
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 4af18f52d3..bae2731aa6 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -350,7 +350,7 @@ let id_of_name = function
   | Anonymous -> raise (Invalid_argument "id_of_name")
 
 let definition_message id =
-  Printer.pr_constant (Global.env ()) id ++ str " is defined"
+  Nameops.pr_id id ++ str " is defined"
     
 let recursive_message v =
   match Array.length v with
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 1bd5bb970c..4933521142 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -115,7 +115,7 @@ val destruct_ex : constr -> constr -> constr list
 
 val id_of_name : name -> identifier
 
-val definition_message : constant -> std_ppcmds
+val definition_message : identifier -> std_ppcmds
 val recursive_message : constant array -> std_ppcmds
 
 val print_message : std_ppcmds -> unit