Merge with lmamane's private branch:

 - New vernac command "Delete"
 - New vernac command "Undo To"
 - Added a few hooks used by new contrib/interface
 - Beta/incomplete version of dependency generation and dumping


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7

27 files changed, 181 insertions, 32 deletions

diff --git a/Makefile.common b/Makefile.common
index f63d7dbcb..1b7a2fef5 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -353,7 +353,8 @@ INTERFACE:=\
   contrib/interface/history.cmo \
   contrib/interface/name_to_ast.cmo contrib/interface/debug_tac.cmo \
   contrib/interface/showproof_ct.cmo contrib/interface/showproof.cmo \
-  contrib/interface/blast.cmo contrib/interface/centaur.cmo
+  contrib/interface/blast.cmo contrib/interface/depends.cmo \
+  contrib/interface/centaur.cmo
 
 INTERFACECMX:=$(INTERFACE:.cmo=.cmx)
 
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index e6b3ba3ec..7d0d134c5 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -446,7 +446,7 @@ let rec pattern_to_term_and_type env typ  = function
       let patl_as_term =
 	List.map2 (pattern_to_term_and_type env)  (List.rev cs_args_types)  patternl
       in
-      mkRApp(mkRRef(Libnames.ConstructRef constr),
+      mkRApp(mkRRef(ConstructRef constr),
 	     implicit_args@patl_as_term
 	    )
 
diff --git a/contrib/interface/COPYRIGHT b/contrib/interface/COPYRIGHT
index ff567a546..23aeb6bb2 100644
--- a/contrib/interface/COPYRIGHT
+++ b/contrib/interface/COPYRIGHT
@@ -1,9 +1,9 @@
 (*****************************************************************************)
 (*                                                                           *)
-(*            Coq support for the Pcoq Graphical Interface of Coq            *)
+(*      Coq support for the Pcoq and tmEgg Graphical Interfaces of Coq       *)
 (*                                                                           *)
 (*        Copyright (C) 1999-2004 INRIA Sophia-Antipolis (Lemme team)        *)
-(*        Copyright (C) 2006 Lionel Elie Mamane                              *)
+(*        Copyright (C) 2006,2007 Lionel Elie Mamane                         *)
 (*                                                                           *)
 (*****************************************************************************)
 
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index a2da3b07d..b82526200 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -8,6 +8,11 @@
  * - Add the backtracking information to the status message.
  * in the following time period
  * - May-November 2006
+ * and
+ * - Make use of new Command.save_hook to generate dependencies at
+ *   save-time.
+ * in
+ *  - June 2007
  *)
 
 (*Toplevel loop for the communication between Coq and Centaur *)
@@ -129,7 +134,7 @@ let print_tree t =
 (*Message functions, the text of these messages is recognized by the protocols *)
 (*of CtCoq                                                                     *)
 let ctf_header message_name request_id =
- fnl () ++ str "message" ++ fnl() ++ str message_name ++ fnl() ++
+ str "message" ++ fnl() ++ str message_name ++ fnl() ++
  int request_id ++ fnl();;
 
 let ctf_acknowledge_command request_id command_count opt_exn =
@@ -749,6 +754,44 @@ let start_default_objects () =
   set_object_pr default_object_pr;
   set_printer_pr default_printer_pr
 
+let full_name_of_ref r =
+  (match r with
+     | VarRef _ -> str "VAR"
+     | ConstRef _ -> str "CST"
+     | IndRef _ -> str "IND"
+     | ConstructRef _ -> str "CSR")
+  ++ str " " ++ (pr_sp (Nametab.sp_of_global r))
+    (* LEM TODO: Cleanly separate path from id (see Libnames.string_of_path) *)
+
+let string_of_ref =
+  (*LEM TODO: Will I need the Var/Const/Ind/Construct info?*)
+  Depends.o Libnames.string_of_path Nametab.sp_of_global
+
+let print_depends compute_depends ptree =
+  output_results (List.fold_left (fun x y -> x ++ (full_name_of_ref y) ++ fnl())
+		    (str "This object depends on:" ++ fnl())
+		    (compute_depends ptree))
+                 None
+
+let output_depends compute_depends ptree =
+  (* Using an ident list for that is arguably stretching it, but less effort than touching the vtp types *)
+  output_results (ctf_header "depends" !global_request_id ++
+		    print_tree (P_ids (CT_id_list (List.map
+						     (fun x -> CT_ident (string_of_ref x))
+						     (compute_depends ptree)))))
+                 None
+
+let gen_start_depends_dumps print_depends print_depends' print_depends'' print_depends''' =
+  Command.set_declare_definition_hook (print_depends' (Depends.depends_of_definition_entry ~acc:[]));
+  Command.set_declare_assumption_hook (print_depends  (fun (c:types) -> Depends.depends_of_constr c []));
+  Command.set_start_hook (print_depends    (fun c -> Depends.depends_of_constr c []));
+  Command.set_save_hook  (print_depends''  (Depends.depends_of_pftreestate Depends.depends_of_pftree));
+  Refiner.set_solve_hook (print_depends''' (fun pt -> Depends.depends_of_pftree_head pt []))
+
+let start_depends_dumps () = gen_start_depends_dumps output_depends output_depends output_depends output_depends
+
+let start_depends_dumps_debug () = gen_start_depends_dumps print_depends print_depends print_depends print_depends
+
 TACTIC EXTEND pbp
 | [ "pbp" ident_opt(idopt) natural_list(nl) ] -> 
     [ if_pcoq pbp_tac_pcoq idopt nl ]
@@ -829,6 +872,10 @@ VERNAC COMMAND EXTEND StartDefaultObjects
 | [ "Start" "Default" "Objects" ] -> [ start_default_objects () ]
 END
 
+VERNAC COMMAND EXTEND StartDependencyDumps
+| [ "Start" "Dependency" "Dumps" ] -> [ start_depends_dumps () ]
+END
+
 VERNAC COMMAND EXTEND StopPcoqHistory
 | [ "Stop" "Pcoq" "History" ] -> [ pcoq_history := false ]
 END
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index bbdbe9a67..49bdfdae1 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -362,7 +362,7 @@ let solve_by_tac evi t =
     Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl
     (fun _ _ -> ());
     Pfedit.by (tclCOMPLETE t);
-    let _,(const,_,_) = Pfedit.cook_proof () in
+    let _,(const,_,_) = Pfedit.cook_proof ignore in
       Pfedit.delete_current_proof (); const.Entries.const_entry_body
   with e ->
     Pfedit.delete_current_proof();
diff --git a/kernel/environ.ml b/kernel/environ.ml
index b1290452a..64bb3a666 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -83,6 +83,7 @@ let fold_rel_context f env ~init =
 (* Named context *)
 
 let named_context_of_val = fst
+let named_vals_of_val = snd
 
 (* [map_named_val f ctxt] apply [f] to the body and the type of
    each declarations.
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 10e962674..19c67435c 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -73,6 +73,7 @@ val fold_rel_context :
 (* Context of variables (section variables and goal assumptions) *)
 
 val named_context_of_val : named_context_val -> named_context
+val named_vals_of_val : named_context_val -> Pre_env.named_vals
 val val_of_named_context : named_context -> named_context_val
 val empty_named_context_val : named_context_val
 
diff --git a/lib/util.ml b/lib/util.ml
index 5e3f7fa6b..29edaf307 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -486,6 +486,18 @@ let list_fold_map' f l e =
 
 let list_map_assoc f = List.map (fun (x,a) -> (x,f a))
 
+(* Specification:
+   - =p= is set equality (double inclusion)
+   - f such that \forall l acc, (f l acc) =p= append (f l []) acc
+   - let g = fun x -> f x [] in
+   - union_map f l acc =p= append (flatten (map g l)) acc
+ *)
+let list_union_map f l acc =
+  List.fold_left
+    (fun x y -> f y x)
+    acc
+    l
+
 (* A generic cartesian product: for any operator (**), 
    [list_cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], 
    and so on if there are more elements in the lists. *)
@@ -761,6 +773,12 @@ let array_distinct v =
   with Exit ->
     false
 
+let array_union_map f a acc =
+  Array.fold_left
+    (fun x y -> f y x)
+    acc
+    a
+
 (* Matrices *)
 
 let matrix_transpose mat =
diff --git a/lib/util.mli b/lib/util.mli
index ae1b906ce..92822f770 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -159,6 +159,7 @@ val list_cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list
 (* list_combinations [[a;b];[c;d]] returns [[a;c];[a;d];[b;c];[b;d]] *)
 val list_combinations : 'a list list -> 'a list list
 
+val list_union_map : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
 
 (*s Arrays. *)
 
@@ -201,6 +202,7 @@ val array_fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
 val array_fold_map2' :
   ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
 val array_distinct : 'a array -> bool
+val array_union_map : ('a -> 'b -> 'b) -> 'a array -> 'b -> 'b
 
 (*s Matrices *)
 
diff --git a/library/lib.ml b/library/lib.ml
index de2047dbd..4acdba88c 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -577,20 +577,44 @@ let recache_context ctx =
 
 let is_frozen_state = function (_,FrozenState _) -> true | _ -> false
 
-let reset_to_gen test =
-  let (_,_,before) = split_lib_gen test in
-  lib_stk := before;
+let set_lib_stk new_lib_stk =
+  lib_stk := new_lib_stk;
   recalc_path_prefix ();
   let spf = match find_entry_p is_frozen_state with
     | (sp, FrozenState f) -> unfreeze_summaries f; sp
     | _ -> assert false
   in
   let (after,_,_) = split_lib spf in
-  let res = recache_context after in
-  res
+  try
+    recache_context after
+  with
+    | Not_found -> error "Tried to set environment to an incoherent state."
+
+let reset_to_gen test =
+  let (_,_,before) = split_lib_gen test in
+  set_lib_stk before
 
 let reset_to sp = reset_to_gen (fun x -> (fst x) = sp)
 
+(* LEM: TODO
+ * We will need to muck with frozen states in after, too!
+ * Not only FrozenState, but also those embedded in Opened(Section|Module|Modtype)
+ *)
+let delete_gen test =
+  let (after,equal,before) = split_lib_gen test in
+  let rec chop_at_dot = function
+    | [] as l -> l
+    | (_, Leaf o)::t when object_tag o = "DOT" -> t
+    | _::t -> chop_at_dot t
+  and chop_before_dot = function
+    | [] as l -> l
+    | (_, Leaf o)::t as l when object_tag o = "DOT" -> l
+    | _::t -> chop_before_dot t
+ in
+  set_lib_stk (List.rev_append (chop_at_dot after) (chop_before_dot before))
+
+let delete sp = delete_gen (fun x -> (fst x) = sp)
+
 let reset_name (loc,id) =
   let (sp,_) = 
     try
@@ -600,6 +624,15 @@ let reset_name (loc,id) =
   in
   reset_to sp
 
+let remove_name (loc,id) =
+  let (sp,_) =
+    try
+      find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi)
+    with Not_found ->
+      user_err_loc (loc,"remove_name",pr_id id ++ str ": no such entry")
+  in
+    delete sp
+
 let is_mod_node = function 
   | OpenedModule _ | OpenedModtype _ | OpenedSection _ 
   | ClosedModule _ | ClosedModtype _ | ClosedSection _  -> true 
@@ -619,15 +652,7 @@ let reset_mod (loc,id) =
     with Not_found ->
       user_err_loc (loc,"reset_mod",pr_id id ++ str ": no such entry")
   in
-  lib_stk := before;
-  recalc_path_prefix ();
-  let spf = match find_entry_p is_frozen_state with
-    | (sp, FrozenState f) -> unfreeze_summaries f; sp
-    | _ -> assert false
-  in
-  let (after,_,_) = split_lib spf in
-  recache_context after
-
+  set_lib_stk before
 
 let mark_end_of_command, current_command_label, set_command_label =
   let n = ref 0 in
diff --git a/library/lib.mli b/library/lib.mli
index 570685585..6c826af63 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -143,6 +143,7 @@ val close_section : identifier -> unit
 
 val reset_to : object_name -> unit
 val reset_name : identifier located -> unit
+val remove_name : identifier located -> unit
 val reset_mod : identifier located -> unit
 
 (* [back n] resets to the place corresponding to the $n$-th call of 
diff --git a/library/libnames.ml b/library/libnames.ml
index dcdd5ac41..dfa0fb82d 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -15,6 +15,7 @@ open Nameops
 open Term
 open Mod_subst
 
+(*s Global reference is a kernel side type for all references together *)
 type global_reference =
   | VarRef of variable
   | ConstRef of constant
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index b564828a5..796636c0e 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -62,6 +62,7 @@ GEXTEND Gram
       | IDENT "Proof"; c = lconstr -> VernacExactProof c
       | IDENT "Undo" -> VernacUndo 1
       | IDENT "Undo"; n = natural -> VernacUndo n
+      | IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo n
       | IDENT "Focus" -> VernacFocus None
       | IDENT "Focus"; n = natural -> VernacFocus (Some n)
       | IDENT "Unfocus" -> VernacUnfocus
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 03c72098c..5c34f2e88 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -749,6 +749,7 @@ GEXTEND Gram
 
 (* Resetting *)
       | IDENT "Reset"; id = identref -> VernacResetName id
+      | IDENT "Delete"; id = identref -> VernacRemoveName id
       | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial
       | IDENT "Back" -> VernacBack 1
       | IDENT "Back"; n = natural -> VernacBack n
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 7e7ea7c56..0daccbba5 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -417,6 +417,7 @@ let rec pr_vernac = function
   | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id
   | VernacResume id -> str"Resume" ++ pr_opt pr_lident id
   | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i
+  | VernacUndoTo i -> str"Undo" ++ spc() ++ str"To" ++ pr_intarg i
   | VernacBacktrack (i,j,k) -> 
       str "Backtrack" ++  spc() ++ prlist_with_sep sep int [i;j;k]
   | VernacFocus i -> str"Focus" ++ pr_opt int i
@@ -446,6 +447,7 @@ let rec pr_vernac = function
   | VernacCheckGuard -> str"Guarded"
 
   (* Resetting *)
+  | VernacRemoveName id -> str"Remove" ++ spc() ++ pr_lident id
   | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id
   | VernacResetInitial -> str"Reset Initial"
   | VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i
diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli
index 4e78a9687..842b85295 100644
--- a/parsing/tactic_printer.mli
+++ b/parsing/tactic_printer.mli
@@ -21,6 +21,7 @@ open Proof_type
 val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds
 val pr_rule     : rule -> std_ppcmds
 val pr_tactic   : tactic_expr -> std_ppcmds
+val pr_proof_instr : Decl_expr.proof_instr -> Pp.std_ppcmds
 val print_script :
   bool -> evar_map -> proof_tree -> std_ppcmds
 val print_treescript :
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index c6cb86dc9..81216d169 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -204,13 +204,14 @@ let current_proof_depth() =
 let xml_cook_proof = ref (fun _ -> ())
 let set_xml_cook_proof f = xml_cook_proof := f
 
-let cook_proof () =
+let cook_proof k =
   let (pfs,ts) = get_state() 
   and ident = get_current_proof_name () in
   let {evar_concl=concl} = ts.top_goal 
   and strength = ts.top_strength in
   let pfterm = extract_pftreestate pfs in
   !xml_cook_proof (strength,pfs);
+  k pfs;
   (ident,
    ({ const_entry_body = pfterm;
       const_entry_type = Some concl;
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index c3d531c69..5de956d46 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -103,7 +103,7 @@ val suspend_proof : unit -> unit
     a constant with its name, kind and possible hook (see [start_proof]);
     it fails if there is no current proof of if it is not completed *)
 
-val cook_proof : unit -> 
+val cook_proof : (Refiner.pftreestate -> unit) -> 
   identifier * (Entries.definition_entry * goal_kind * declaration_hook)
 
 (* To export completed proofs to xml *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 7010153ba..85f8a4f0e 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -108,13 +108,23 @@ let rec frontier p =
 		  open_subgoals = and_status (List.map pf_status pfl');
 		  ref = Some(r,pfl')}))
 
+(* TODO LEM: I might have to make sure that these hooks are called
+   only when called from solve_nth_pftreestate; I can build the hook
+   call into the "f", then.
+ *)
+let solve_hook = ref ignore
+let set_solve_hook = (:=) solve_hook
 
 let rec frontier_map_rec f n p =
   if n < 1 || n > p.open_subgoals then p else
   match p.ref with
     | None -> 
         let p' = f p in
-        if Evd.eq_evar_info p'.goal p.goal then p'
+        if Evd.eq_evar_info p'.goal p.goal then
+	  begin
+	    !solve_hook p';
+	    p'
+	  end
         else 
 	  errorlabstrm "Refiner.frontier_map"
             (str"frontier_map was handed back a ill-formed proof.")
@@ -140,7 +150,11 @@ let rec frontier_mapi_rec f i p =
   match p.ref with
     | None -> 
         let p' = f i p in
-        if Evd.eq_evar_info p'.goal p.goal then p'
+        if Evd.eq_evar_info p'.goal p.goal then
+	  begin
+	    !solve_hook p';
+	    p'
+	  end
         else 
 	  errorlabstrm "Refiner.frontier_mapi"
             (str"frontier_mapi was handed back a ill-formed proof.")
@@ -849,6 +863,7 @@ let prev_unproven pts =
 let rec top_of_tree pts = 
   if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
 
+(* FIXME: cette fonction n'est (as of October 2007) appelée nulle part *)
 let change_rule f pts =
   let mark_top _ pt =
     match pt.ref with
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index e79534b38..af9da961b 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -48,6 +48,8 @@ val list_pf : proof_tree -> goal list
 val unTAC : tactic -> goal sigma -> proof_tree sigma
 
 
+(* Install a hook frontier_map and frontier_mapi call on the new node they create *)
+val set_solve_hook : (Proof_type.proof_tree -> unit) -> unit
 (* [frontier_map f n p] applies f on the n-th open subgoal of p and
    rebuilds proof-tree.
    n=1 for first goal, n negative counts from the right *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 24149a98e..effd6f9af 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1300,7 +1300,7 @@ let solvable_by_tactic env evi (ev,args) src =
       begin
 	try
 	  by (tclCOMPLETE tac);
-	  let _,(const,_,_) = cook_proof () in 
+	  let _,(const,_,_) = cook_proof ignore in 
 	  delete_current_proof (); const.const_entry_body
 	with e when Logic.catchable_exception e -> 
 	  delete_current_proof();
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index fa40e1651..611918543 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2691,7 +2691,7 @@ let abstract_subproof name tac gl =
       let _,(const,kind,_) =
 	try
 	  by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); 
-	  let r = cook_proof () in 
+	  let r = cook_proof ignore in 
 	    delete_current_proof (); r
 	with 
 	    e ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9ccd2ff2e..ccdb906ce 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -146,9 +146,13 @@ let declare_global_definition ident ce local imps =
     definition_message ident;
     gr
 
+let declare_definition_hook = ref ignore
+let set_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
   let ce' = red_constant_entry bl ce red_option in
+  !declare_definition_hook ce';
   let r = match local with
     | Local when Lib.sections_are_opened () ->
         let c =
@@ -194,10 +198,14 @@ let declare_one_assumption is_coe (local,kind) c nl (_,ident) =
         ConstRef kn in
   if is_coe then Class.try_add_new_coercion r local
 
+let declare_assumption_hook = ref ignore
+let set_declare_assumption_hook = (:=) declare_assumption_hook
+
 let declare_assumption idl is_coe k bl c nl=
   if not (Pfedit.refining ()) then 
     let c = generalize_constr_expr c bl in
     let c = interp_type Evd.empty (Global.env()) c in
+      !declare_assumption_hook c;
       List.iter (declare_one_assumption is_coe k c nl) idl
   else
     errorlabstrm "Command.Assumption"
@@ -334,10 +342,14 @@ let (inDec,outDec) =
                     subst_function = Auto_ind_decl.subst_in_constr;
                     export_function = Ind_tables.export_dec_proof }
 
+let start_hook = ref ignore
+let set_start_hook = (:=) start_hook
+
 let start_proof id kind c hook =
   let sign = Global.named_context () in
   let sign = clear_proofs sign in
-  Pfedit.start_proof id kind sign c hook
+    !start_hook c;
+    Pfedit.start_proof id kind sign c hook
 
 let save id const (locality,kind) hook =
   let {const_entry_body = pft;
@@ -361,8 +373,11 @@ let save id const (locality,kind) hook =
   definition_message id;
   hook l r
 
+let save_hook = ref ignore
+let set_save_hook f = save_hook := f
+
 let save_named opacity =
-  let id,(const,persistence,hook) = Pfedit.cook_proof () in
+  let id,(const,persistence,hook) = Pfedit.cook_proof !save_hook in
   let const = { const with const_entry_opaque = opacity } in
   save id const persistence hook
 
@@ -1023,13 +1038,13 @@ let check_anonymity id save_ident =
 *)
 
 let save_anonymous opacity save_ident =
-  let id,(const,persistence,hook) = Pfedit.cook_proof () in
+  let id,(const,persistence,hook) = Pfedit.cook_proof !save_hook in
   let const = { const with const_entry_opaque = opacity } in
   check_anonymity id save_ident;
   save save_ident const persistence hook
 
 let save_anonymous_with_strength kind opacity save_ident =
-  let id,(const,_,hook) = Pfedit.cook_proof () in
+  let id,(const,_,hook) = Pfedit.cook_proof !save_hook in
   let const = { const with const_entry_opaque = opacity } in
   check_anonymity id save_ident;
   (* we consider that non opaque behaves as local for discharge *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 7ec29e0f5..2dbc29538 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -30,6 +30,8 @@ open Redexpr
    functions of [Declare]; they return an absolute reference to the
    defined object *)
 
+val set_declare_definition_hook : (Entries.definition_entry -> unit) -> unit
+
 val definition_message : identifier -> unit
 
 val declare_definition : identifier -> definition_kind ->
@@ -41,6 +43,8 @@ val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit
 val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types -> bool
   -> Names.variable located  -> unit
 
+val set_declare_assumption_hook : (types -> unit) -> unit
+
 val declare_assumption : identifier located list ->
   coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> bool 
   ->unit
@@ -93,12 +97,18 @@ val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr
 
 val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
 
-val start_proof : identifier -> goal_kind -> constr ->
+(* A hook start_proof calls on the type of the definition being started *)
+val set_start_hook : (types -> unit) -> unit
+
+val start_proof : identifier -> goal_kind -> types ->
   declaration_hook -> unit
 
 val start_proof_com : identifier option -> goal_kind -> 
   (local_binder list * constr_expr) -> declaration_hook -> unit
 
+(* A hook the next three functions pass to cook_proof *)
+val set_save_hook : (Refiner.pftreestate -> unit) -> unit
+
 (*s [save_named b] saves the current completed proof under the name it
 was started; boolean [b] tells if the theorem is declared opaque; it
 fails if the proof is not completed *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ec60cc52e..13b2bab5c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1251,6 +1251,7 @@ let interp c = match c with
   | VernacRestoreState s -> vernac_restore_state s
 
   (* Resetting *)
+  | VernacRemoveName id -> Lib.remove_name id
   | VernacResetName id -> vernac_reset_name id
   | VernacResetInitial -> vernac_reset_initial ()
   | VernacBack n -> vernac_back n
@@ -1285,6 +1286,7 @@ let interp c = match c with
   | VernacSuspend -> vernac_suspend ()
   | VernacResume id -> vernac_resume id
   | VernacUndo n -> vernac_undo n
+  | VernacUndoTo n -> undo_todepth n
   | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts
   | VernacFocus n -> vernac_focus n
   | VernacUnfocus -> vernac_unfocus ()
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 65464d4e2..6cbb53617 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -47,7 +47,7 @@ type pcoq_hook = {
 
 val set_pcoq_hook : pcoq_hook -> unit
 
-(* This function makes sure that the function given is argument is preceded
+(* This function makes sure that the function given in argument is preceded
    by a command aborting all proofs if necessary.
    It is used in pcoq. *)
 val abort_refine : ('a -> unit) -> 'a -> unit;;
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index cf7fb72c6..a25cd09e7 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -276,6 +276,7 @@ type vernac_expr =
   | VernacRestoreState of lstring
 
   (* Resetting *)
+  | VernacRemoveName of lident
   | VernacResetName of lident
   | VernacResetInitial
   | VernacBack of int
@@ -313,6 +314,7 @@ type vernac_expr =
   | VernacSuspend
   | VernacResume of lident option
   | VernacUndo of int
+  | VernacUndoTo of int
   | VernacBacktrack of int*int*int
   | VernacFocus of int option
   | VernacUnfocus