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://scm.gforge.inria.fr/svn/coq/trunk@11024 85f007b7-540e-0410-9357-904b9bb8a0f7

Author: msozeau

contrib/funind/g_indfun.ml4

@@ -183,7 +183,7 @@ VERNAC ARGUMENT EXTEND rec_definition2
 	 | Some an ->
 	     check_exists_args an
      in
-     (id, ni, bl, type_, def) ]
+     ((Util.dummy_loc,id), ni, bl, type_, def) ]
       END
 
 

contrib/funind/indfun.ml

@@ -160,7 +160,7 @@ let build_newrecursive
   in
   let (rec_sign,rec_impls) =
     List.fold_left
-      (fun (env,impls) (recname,_,bl,arityc,_) ->
+      (fun (env,impls) ((_,recname),_,bl,arityc,_) ->
         let arityc = Command.generalize_constr_expr arityc bl in
         let arity = Constrintern.interp_type sigma env0 arityc in
 	let impl =
@@ -297,7 +297,7 @@ let generate_principle  on_error
     is_general do_built fix_rec_l recdefs  interactive_proof 
     (continue_proof : int -> Names.constant array -> Term.constr array -> int -> 
       Tacmach.tactic) : unit =
-  let names = List.map (function (name,_,_,_,_) -> name) fix_rec_l in
+  let names = List.map (function ((_, name),_,_,_,_) -> name) fix_rec_l in
   let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
   let funs_args = List.map fst fun_bodies in
   let funs_types =  List.map (function (_,_,_,types,_) -> types) fix_rec_l in
@@ -318,7 +318,7 @@ let generate_principle  on_error
 		 f_R_mut)
 	in
 	let fname_kn (fname,_,_,_,_) =
-	  let f_ref = Ident (dummy_loc,fname) in
+	  let f_ref = Ident fname in
 	  locate_with_msg
 	    (pr_reference f_ref++str ": Not an inductive type!")
 	    locate_constant
@@ -351,7 +351,7 @@ let generate_principle  on_error
 
 let register_struct is_rec fixpoint_exprl = 
   match fixpoint_exprl with 
-    | [(fname,_,bl,ret_type,body),_] when not is_rec -> 
+    | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> 
 	Command.declare_definition
 	  fname
 	  (Decl_kinds.Global,Flags.boxed_definitions (),Decl_kinds.Definition)
@@ -475,7 +475,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
   let recdefs,rec_impls = build_newrecursive fixpoint_exprl in 
   let _is_struct = 
     match fixpoint_exprl with 
-      | [((name,Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> 
+      | [(((_,name),Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> 
 	  let pre_hook = 
 	    generate_principle 
 	      on_error
@@ -488,7 +488,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
 	  if register_built 
 	  then register_wf name rec_impls wf_rel wf_x using_lemmas args types body pre_hook;
 	  false
-      | [((name,Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> 
+      | [(((_,name),Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> 
 	  let pre_hook = 
 	    generate_principle 
 	      on_error
@@ -503,7 +503,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
 	  true
       | _ -> 
 	  let fix_names = 
-	    List.map (function (name,_,_,_,_) -> name) fixpoint_exprl 
+	    List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl 
 	  in
 	  let is_one_rec = is_rec fix_names  in
 	  let old_fixpoint_exprl =  
@@ -535,7 +535,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
 	  in
 	  (* ok all the expressions are structural *) 
 	  let fix_names = 
-	    List.map (function (name,_,_,_,_) -> name) fixpoint_exprl 
+	    List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl 
 	  in
 	  let is_rec = List.exists (is_rec fix_names) recdefs in
 	  if register_built then register_struct is_rec old_fixpoint_exprl;
@@ -724,21 +724,21 @@ let make_graph (f_ref:global_reference) =
 			      nal_tas
 			   )
 		       in
-		       let b' = add_args id new_args b in 
+		       let b' = add_args (snd id) new_args b in 
 		       (id, Some (Struct rec_id),nal_tas@bl,t,b')
 		    )
 		    fixexprl
 		in
 		l
 	    | _ ->   
 		let id = id_of_label (con_label c) in 
-		[(id,None,nal_tas,t,b)]
+		[((dummy_loc,id),None,nal_tas,t,b)]
 	in
 	do_generate_principle error_error false false expr_list;
 	(* We register the infos *)
 	let mp,dp,_ = repr_con c in 
 	List.iter 
-	  (fun (id,_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id))) 
+	  (fun ((_,id),_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id))) 
 	  expr_list
 
 

contrib/interface/xlate.ml

@@ -414,13 +414,13 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
        xlate_error "Second order variable not supported"
    | CEvar _ -> xlate_error "CEvar not supported"
    | CCoFix (_, (_, id), lm::lmi) -> 
-     let strip_mutcorec (fid, bl,arf, ardef) =
+     let strip_mutcorec ((_, fid), bl,arf, ardef) =
 	CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
                       xlate_formula arf, xlate_formula ardef) in
         CT_cofixc(xlate_ident id,
 	  (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)))
    | CFix (_, (_, id), lm::lmi) ->       
-     let strip_mutrec (fid, (n, ro), bl, arf, ardef) =
+     let strip_mutrec ((_, fid), (n, ro), bl, arf, ardef) =
         let struct_arg = make_fix_struct (n, bl) in
         let arf = xlate_formula arf in
         let ardef = xlate_formula ardef in
@@ -1939,7 +1939,7 @@ let rec xlate_vernac =
 	  (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi))
    | VernacFixpoint ([],_) -> xlate_error "mutual recursive"
    | VernacFixpoint ((lm :: lmi),boxed) ->
-      let strip_mutrec ((fid, (n, ro), bl, arf, ardef), _ntn) =
+      let strip_mutrec (((_,fid), (n, ro), bl, arf, ardef), _ntn) =
         let struct_arg = make_fix_struct (n, bl) in
         let arf = xlate_formula arf in
         let ardef = xlate_formula ardef in
@@ -1952,7 +1952,7 @@ let rec xlate_vernac =
 	  (CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi))
    | VernacCoFixpoint ([],boxed) -> xlate_error "mutual corecursive"
    | VernacCoFixpoint ((lm :: lmi),boxed) ->
-      let strip_mutcorec ((fid, bl, arf, ardef), _ntn) =
+      let strip_mutcorec (((_,fid), bl, arf, ardef), _ntn) =
 	CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
                       xlate_formula arf, xlate_formula ardef) in
         CT_cofix_decl
@@ -1974,9 +1974,9 @@ let rec xlate_vernac =
         CT_ind_scheme
 	  (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi))
    | VernacCombinedScheme _ -> xlate_error "TODO: Combined Scheme"
-   | VernacSyntacticDefinition (id, ([],c), false, _) ->
+   | VernacSyntacticDefinition ((_,id), ([],c), false, _) ->
        CT_syntax_macro (xlate_ident id, xlate_formula c, xlate_int_opt None)
-   | VernacSyntacticDefinition (id, _, _, _) ->
+   | VernacSyntacticDefinition ((_,id), _, _, _) ->
        xlate_error"TODO: Local abbreviations and abbreviations with parameters"
   (* Modules and Module Types *)
    | VernacInclude (_) -> xlate_error "TODO : Include "

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*)

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

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,22 +430,22 @@ 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
       | _, _ -> 
 	  errorlabstrm "Subtac_command.build_recursive"
 	    (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