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

5 files changed, 35 insertions, 6 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9ccd2ff2e6..ccdb906cec 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 7ec29e0f59..2dbc295387 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 ec60cc52ed..13b2bab5cb 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 65464d4e2d..6cbb536175 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 cf7fb72c67..a25cd09e74 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