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

13 files changed, 103 insertions, 67 deletions

diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4
index 4b3492b125..71f483fb61 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/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
 
 
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index fa49d4aa86..a071add636 100644
--- a/contrib/funind/indfun.ml
+++ b/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,7 +724,7 @@ 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
@@ -732,13 +732,13 @@ let make_graph (f_ref:global_reference) =
 		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
 
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 169ec0dc22..c2569a1428 100644
--- a/contrib/interface/xlate.ml
+++ b/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 "
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
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 7e3a1bd410..3c4b01f5bb 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -487,7 +487,10 @@ let kind_of_constant kn =
     | DK.IsDefinition DK.Instance ->
         Pp.warning "Instance not supported in dtd (used Definition instead)";
         "DEFINITION","Definition" 
-   | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) ->
+    | DK.IsDefinition DK.Method ->
+        Pp.warning "Method not supported in dtd (used Definition instead)";
+        "DEFINITION","Definition" 
+    | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) ->
         "THEOREM",DK.string_of_theorem_kind thm
     | DK.IsProof _ ->
         Pp.warning "Unsupported theorem kind (used Theorem instead)";