The commands that initiate proofs are now in charge of what happens when proofs end.

The proof ending commands like Qed and Defined had all the control on what happened to the proof when they are closed. In constrast, proof starting commands were dumb: start a proof, give it a name, that's it.

In such a situation if we want to come up with new reasons to open proofs, we would need new proof-closing commands.

In this commit we decide at proof-starting time how to dispatch the various Qed/Defined, etc… By registering a function in the interactive proof environment. This way, proofs are always closed the same but we can invent new ways to start them.

13 files changed, 160 insertions, 139 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 52ba41869a..f4e8589031 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -983,7 +983,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
     lemma_type
     (fun _ _ -> ());
   ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
-  Lemmas.save_named false
+  Lemmas.save_proof (Vernacexpr.Proved(false,None))
 
 
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index b7072ea3bd..db4297b37d 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -169,11 +169,6 @@ let cook_proof _ =
   let (id,(entry,_,strength,hook)) = Pfedit.cook_proof (fun _ -> ()) in
   (id,(entry,strength,hook))
 
-let new_save_named opacity =
-  let id,(const,persistence,hook) = cook_proof true  in
-  let const = { const with const_entry_opaque = opacity } in
-  save true id const persistence hook
-
 let get_proof_clean do_reduce =
   let result = cook_proof do_reduce in
   Pfedit.delete_current_proof ();
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 722f857b34..cea5ffe259 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -46,12 +46,6 @@ val const_of_id: Id.t -> constant
 val jmeq : unit -> Term.constr
 val jmeq_refl : unit -> Term.constr
 
-(* [save_named] is a copy of [Command.save_named] but uses
-   [nf_betaiotazeta] instead of [nf_betaiotaevar_preserving_vm_cast]
-*)
-
-val new_save_named : bool -> unit
-
 val save : bool -> Id.t ->  Entries.definition_entry  -> Decl_kinds.goal_kind ->
   unit Tacexpr.declaration_hook Ephemeron.key -> unit
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 0d32bf2bc9..7c8f5714e6 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1008,7 +1008,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 
 
 
-let do_save () = Lemmas.save_named false
+let do_save () = Lemmas.save_proof (Vernacexpr.Proved(false,None))
 
 
 (* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 6afbff779d..082d7ad51e 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -64,7 +64,7 @@ let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) =
           const_entry_inline_code = false} in
       ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
 
-let defined () = Lemmas.save_named false
+let defined () = Lemmas.save_proof (Vernacexpr.Proved (false,None))
 
 let def_of_const t =
    match (kind_of_term t) with
@@ -1249,7 +1249,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	with e when Errors.noncritical e ->
           anomaly (Pp.str "open_new_goal with an unamed theorem")
   in
-  let sign = initialize_named_context_for_proof () in
   let na = next_global_ident_away name [] in
   if Termops.occur_existential gls_type then
     Errors.error "\"abstract\" cannot handle existentials";
@@ -1309,12 +1308,11 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	       )
       		 g)
 ;
-    Lemmas.save_named opacity;
+    Lemmas.save_proof (Vernacexpr.Proved(opacity,None));
   in
-  start_proof
+  Lemmas.start_proof
     na
     (Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma)
-    sign
     gls_type
     hook;
   if Indfun_common.is_strict_tcc  ()
@@ -1360,8 +1358,8 @@ let com_terminate
     hook =
   let start_proof (tac_start:tactic) (tac_end:tactic) =
     let (evmap, env) = Lemmas.get_current_context() in
-    start_proof thm_name
-      (Global, Proof Lemma) (Environ.named_context_val env)
+    Lemmas.start_proof thm_name
+      (Global, Proof Lemma) ~sign:(Environ.named_context_val env)
       (compute_terminate_type nb_args fonctional_ref) hook;
 
     ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start)));
@@ -1408,8 +1406,8 @@ let (com_eqn : int -> Id.t ->
     let (evmap, env) = Lemmas.get_current_context() in
     let f_constr = constr_of_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
-    (start_proof eq_name (Global, Proof Lemma)
-       (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
+    (Lemmas.start_proof eq_name (Global, Proof Lemma)
+       ~sign:(Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
      ignore (by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
 	  (fun  x ->
@@ -1440,7 +1438,7 @@ let (com_eqn : int -> Id.t ->
        ))); 
      (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
 (*      Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
-     Flags.silently (fun () -> Lemmas.save_named opacity) () ; 
+     Flags.silently (fun () -> Lemmas.save_proof (Vernacexpr.Proved(opacity,None))) () ; 
 (*      Pp.msgnl (str "eqn finished"); *)
     );;
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 8a52244df2..e4cdf49896 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -29,9 +29,9 @@ let delete_all_proofs = Proof_global.discard_all
 let set_undo _ = ()
 let get_undo _ = None
 
-let start_proof (id : Id.t) str hyps c ?init_tac ?compute_guard hook =
+let start_proof (id : Id.t) str hyps c ?init_tac ?compute_guard hook terminator =
   let goals = [ (Global.env_of_context hyps , c) ] in
-  Proof_global.start_proof id str goals ?compute_guard hook;
+  Proof_global.start_proof id str goals ?compute_guard hook terminator;
   let env = Global.env () in
   ignore (Proof_global.with_current_proof (fun _ p ->
     match init_tac with
@@ -40,11 +40,12 @@ let start_proof (id : Id.t) str hyps c ?init_tac ?compute_guard hook =
 
 let cook_this_proof hook p =
   match p with
-  | (i,([e],cg,str,h)) -> (i,(e,cg,str,h))
+  | { Proof_global.id;entries=[constr];do_guard;persistence;hook } ->
+      (id,(constr,do_guard,persistence,hook))
   | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
 
 let cook_proof hook =
-  cook_this_proof hook (Proof_global.close_proof (fun x -> x))
+  cook_this_proof hook (fst (Proof_global.close_proof (fun x -> x)))
 let get_pftreestate () =
   Proof_global.give_me_the_proof ()
 
@@ -122,7 +123,7 @@ open Decl_kinds
 let next = let n = ref 0 in fun () -> incr n; !n
 
 let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac =
-  start_proof id goal_kind sign typ (fun _ _ -> ());
+  start_proof id goal_kind sign typ (fun _ _ -> ()) (fun _ -> ());
   try
     let status = by tac in
     let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
@@ -166,13 +167,3 @@ let solve_by_implicit_tactic env sigma evk =
       (try fst (build_by_tactic env evi.evar_concl (Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (Errors.UserError ("",Pp.str"Proof is not complete."))) [])))
        with e when Logic.catchable_exception e -> raise Exit)
   | _ -> raise Exit
-
-
-
-
-
-
-
-
-
-
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 6dad738afb..110df23470 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -62,7 +62,7 @@ type lemma_possible_guards = Proof_global.lemma_possible_guards
 val start_proof :
   Id.t -> goal_kind -> named_context_val -> constr ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
-  unit declaration_hook -> unit
+  unit declaration_hook -> Proof_global.proof_terminator -> unit
 
 (** {6 ... } *)
 (** [cook_proof opacity] turns the current proof (assumed completed) into
@@ -71,19 +71,15 @@ val start_proof :
     it also tells if the guardness condition has to be inferred. *)
 
 val cook_this_proof : (Proof.proof -> unit) ->
-    Id.t *
-    (Entries.definition_entry list *
-    lemma_possible_guards *
-    Decl_kinds.goal_kind *
-    unit Tacexpr.declaration_hook Ephemeron.key) ->
-  Id.t *
+    Proof_global.proof_object ->
+  (Id.t *
     (Entries.definition_entry * lemma_possible_guards * goal_kind *
-     unit declaration_hook Ephemeron.key)
+     unit declaration_hook Ephemeron.key))
 
 val cook_proof : (Proof.proof -> unit) ->
-  Id.t *
+  (Id.t *
     (Entries.definition_entry * lemma_possible_guards * goal_kind *
-     unit declaration_hook Ephemeron.key)
+     unit declaration_hook Ephemeron.key))
 
 (** {6 ... } *)
 (** [get_pftreestate ()] returns the current focused pending proof.
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index b7a32a9801..b2282a6831 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -65,14 +65,28 @@ let _ =
 (* Extra info on proofs. *)
 type lemma_possible_guards = int list list
 
+type proof_object = {
+  id : Names.Id.t;
+  entries : Entries.definition_entry list;
+  do_guard : lemma_possible_guards;
+  persistence : Decl_kinds.goal_kind;
+  hook : unit Tacexpr.declaration_hook Ephemeron.key
+}
+
+type proof_ending = Vernacexpr.proof_end * proof_object
+type proof_terminator =
+    proof_ending -> unit
+type closed_proof = proof_object*proof_terminator Ephemeron.key
+
 type pstate = {
   pid : Id.t;
+  terminator : proof_terminator Ephemeron.key;
   endline_tactic : Tacexpr.raw_tactic_expr option;
   section_vars : Context.section_context option;
   proof : Proof.proof;
   strength : Decl_kinds.goal_kind;
   compute_guard : lemma_possible_guards;
-  hook : unit Tacexpr.declaration_hook Ephemeron.key;
+  pr_hook : unit Tacexpr.declaration_hook Ephemeron.key;
   mode : proof_mode Ephemeron.key;
 }
 
@@ -236,27 +250,29 @@ end
     It raises exception [ProofInProgress] if there is a proof being
     currently edited. *)
 
-let start_proof id str goals ?(compute_guard=[]) hook =
+let start_proof id str goals ?(compute_guard=[]) hook terminator =
   let initial_state = {
     pid = id;
+    terminator = Ephemeron.create terminator;
     proof = Proof.start Evd.empty goals;
     endline_tactic = None;
     section_vars = None;
     strength = str;
     compute_guard = compute_guard;
-    hook = Ephemeron.create hook;
+    pr_hook = Ephemeron.create hook;
     mode = find_proof_mode "No" } in
   push initial_state pstates
 
-let start_dependent_proof id str goals ?(compute_guard=[]) hook =
+let start_dependent_proof id str goals ?(compute_guard=[]) hook terminator =
   let initial_state = {
     pid = id;
+    terminator = Ephemeron.create terminator;
     proof = Proof.dependent_start Evd.empty goals;
     endline_tactic = None;
     section_vars = None;
     strength = str;
     compute_guard = compute_guard;
-    hook = Ephemeron.create hook;
+    pr_hook = Ephemeron.create hook;
     mode = find_proof_mode "No" } in
   push initial_state pstates
 
@@ -280,13 +296,10 @@ let get_open_goals () =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
   List.length shelf
 
-type closed_proof =
-  Names.Id.t *
-  (Entries.definition_entry list * lemma_possible_guards *
-    Decl_kinds.goal_kind * unit Tacexpr.declaration_hook Ephemeron.key)
-
 let close_proof ~now fpl =
-  let { pid;section_vars;compute_guard;strength;hook;proof } = cur_pstate () in
+  let { pid;section_vars;compute_guard;strength;pr_hook;proof;terminator } =
+    cur_pstate ()
+  in
   let initial_goals = Proof.initial_goals proof in
   let entries = Future.map2 (fun p (c, t) -> { Entries.
     const_entry_body = p;
@@ -296,7 +309,11 @@ let close_proof ~now fpl =
     const_entry_opaque = true }) fpl initial_goals in
   if now then
     List.iter (fun x -> ignore(Future.join x.Entries.const_entry_body)) entries;
-  (pid, (entries, compute_guard, strength, hook))
+  { id = pid ;
+    entries = entries ;
+    do_guard = compute_guard ;
+    persistence = strength ;
+    hook = pr_hook } , terminator
 
 let return_proof () =
   let { proof } = cur_pstate () in
@@ -471,8 +488,8 @@ let _ =
 
 module V82 = struct
   let get_current_initial_conclusions () =
-    let { pid; strength; hook; proof } = cur_pstate () in
-    pid, (List.map snd (Proof.initial_goals proof), strength, hook)
+    let { pid; strength; pr_hook; proof } = cur_pstate () in
+    pid, (List.map snd (Proof.initial_goals proof), strength, pr_hook)
 end
 
 type state = pstate list
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index e88c2f3942..eb7d0ecb17 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -46,17 +46,37 @@ exception NoCurrentProof
 val give_me_the_proof : unit -> Proof.proof
 (** @raise NoCurrentProof when outside proof mode. *)
 
+(** When a proof is closed, it is reified into a [proof_object], where
+    [id] is the name of the proof, [entries] the list of the proof terms
+    (in a form suitable for definitions). Together with the [terminator]
+    function which takes a [proof_object] together with a [proof_end]
+    (i.e. an proof ending command) and registers the appropriate
+    values. *)
+type lemma_possible_guards = int list list
+type proof_object = {
+  id : Names.Id.t;
+  entries : Entries.definition_entry list;
+  do_guard : lemma_possible_guards;
+  persistence : Decl_kinds.goal_kind;
+  hook : unit Tacexpr.declaration_hook Ephemeron.key
+}
+
+type proof_ending = Vernacexpr.proof_end * proof_object
+type proof_terminator =
+    proof_ending -> unit
+type closed_proof = proof_object*proof_terminator Ephemeron.key
+
 (** [start_proof s str goals ~init_tac ~compute_guard hook] starts 
     a proof of name [s] and
     conclusion [t]; [hook] is optionally a function to be applied at
     proof end (e.g. to declare the built constructions as a coercion
     or a setoid morphism). *)
-type lemma_possible_guards = int list list
 val start_proof : Names.Id.t ->
                           Decl_kinds.goal_kind ->
                           (Environ.env * Term.types) list  ->
-                          ?compute_guard:lemma_possible_guards -> 
-                          unit Tacexpr.declaration_hook -> 
+                          ?compute_guard:lemma_possible_guards ->
+                          unit Tacexpr.declaration_hook ->
+                          proof_terminator ->
                           unit
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
@@ -65,12 +85,9 @@ val start_dependent_proof : Names.Id.t ->
                           Proofview.telescope  ->
                           ?compute_guard:lemma_possible_guards ->
                           unit Tacexpr.declaration_hook ->
+                          proof_terminator ->
                           unit
 
-type closed_proof =
-  Names.Id.t *
-  (Entries.definition_entry list * lemma_possible_guards *
-    Decl_kinds.goal_kind * unit Tacexpr.declaration_hook Ephemeron.key)
 
 (* Takes a function to add to the exceptions data relative to the
    state in which the proof was built *)
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 20b792cc07..db479615ef 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -169,7 +169,7 @@ let look_for_possibly_mutual_statements = function
 
 (* Saving a goal *)
 
-let save ?proof id const do_guard (locality,kind) hook =
+let save id const do_guard (locality,kind) hook =
   let const = adjust_guardness_conditions const do_guard in
   let k = Kindops.logical_kind_of_goal_kind kind in
   let l,r = match locality with
@@ -185,8 +185,6 @@ let save ?proof id const do_guard (locality,kind) hook =
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
 	Autoinstance.search_declaration (ConstRef kn);
 	(locality, ConstRef kn) in
-  (* if the proof is given explicitly, nothing has to be deleted *)
-  if Option.is_empty proof then Pfedit.delete_current_proof ();
   definition_message id;
   Ephemeron.iter_opt hook (fun f -> f l r)
 
@@ -260,42 +258,75 @@ let save_remaining_recthms (locality,kind) body opaq i (id,(t_i,(_,imps))) =
 let save_hook = ref ignore
 let set_save_hook f = save_hook := f
 
-let get_proof ?proof opacity =
-  let id,(const,do_guard,persistence,hook) = 
-    match proof with
-    | None -> Pfedit.cook_proof !save_hook 
-    | Some p -> Pfedit.cook_this_proof !save_hook p in
-  id,{const with const_entry_opaque = opacity},do_guard,persistence,hook
-
-let save_named ?proof opacity =
-  let id,const,do_guard,persistence,hook = get_proof ?proof opacity in
-  save ?proof id const do_guard persistence hook
+let save_named proof =
+  let id,const,do_guard,persistence,hook = proof in
+  save id const do_guard persistence hook
 
 let check_anonymity id save_ident =
   if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
     error "This command can only be used for unnamed theorem."
 
 
-let save_anonymous ?proof opacity save_ident =
-  let id,const,do_guard,persistence,hook = get_proof ?proof opacity in
+let save_anonymous proof save_ident =
+  let id,const,do_guard,persistence,hook = proof in
   check_anonymity id save_ident;
-  save ?proof save_ident const do_guard persistence hook
+  save save_ident const do_guard persistence hook
 
-let save_anonymous_with_strength ?proof kind opacity save_ident =
-  let id,const,do_guard,_,hook = get_proof ?proof opacity in
+let save_anonymous_with_strength proof kind save_ident =
+  let id,const,do_guard,_,hook = proof in
   check_anonymity id save_ident;
   (* we consider that non opaque behaves as local for discharge *)
-  save ?proof save_ident const do_guard (Global, Proof kind) hook
+  save save_ident const do_guard (Global, Proof kind) hook
+
+(* Admitted *)
+
+let admit () =
+  let (id,k,typ,hook) = Pfedit.current_proof_statement () in
+  let e = Pfedit.get_used_variables(), typ, None in
+  let kn = declare_constant id (ParameterEntry e,IsAssumption Conjectural) in
+  let () = match fst k with
+  | Global -> ()
+  | Local | Discharge ->
+    msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
+      str "declared as an axiom.")
+  in
+  let () = assumption_message id in
+  Ephemeron.iter_opt hook (fun f -> f Global (ConstRef kn))
 
 (* Starting a goal *)
 
 let start_hook = ref ignore
 let set_start_hook = (:=) start_hook
 
-let start_proof id kind c ?init_tac ?(compute_guard=[]) hook =
-  let sign = initialize_named_context_for_proof () in
+
+let get_proof proof opacity =
+  let (id,(const,do_guard,persistence,hook)) =
+    Pfedit.cook_this_proof !save_hook proof
+  in
+  id,{const with const_entry_opaque = opacity},do_guard,persistence,hook
+
+let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook =
+  let terminator = let open Vernacexpr in function
+    | Admitted,_ ->
+        admit ();
+        Pp.feedback Interface.AddedAxiom
+    | Proved (is_opaque,idopt),proof ->
+        let proof = get_proof proof is_opaque in
+        begin match idopt with
+        | None -> save_named proof
+        | Some ((_,id),None) -> save_anonymous proof id
+        | Some ((_,id),Some kind) -> 
+            save_anonymous_with_strength proof kind id
+        end
+  in
+  let sign = 
+    match sign with
+    | Some sign -> sign
+    | None -> initialize_named_context_for_proof ()
+  in
   !start_hook c;
-  Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook
+  Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook terminator
+
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
@@ -365,21 +396,18 @@ let start_proof_com kind thms hook =
   let recguard,thms,snl = look_for_possibly_mutual_statements thms in
   start_proof_with_initialization kind recguard thms snl hook
 
-(* Admitted *)
 
-let admit () =
-  let (id,k,typ,hook) = Pfedit.current_proof_statement () in
-  let e = Pfedit.get_used_variables(), typ, None in
-  let kn = declare_constant id (ParameterEntry e,IsAssumption Conjectural) in
-  let () = Pfedit.delete_current_proof () in
-  let () = match fst k with
-  | Global -> ()
-  | Local | Discharge ->
-    msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++
-      str "declared as an axiom.")
+(* Saving a proof *)
+
+let save_proof ?proof ending =
+  let (proof_obj,terminator) =
+    match proof with
+    | None -> Proof_global.close_proof (fun x -> x)
+    | Some proof -> proof
   in
-  let () = assumption_message id in
-  Ephemeron.iter_opt hook (fun f -> f Global (ConstRef kn))
+  (* if the proof is given explicitly, nothing has to be deleted *)
+  if Option.is_empty proof then Pfedit.delete_current_proof ();
+  Ephemeron.get terminator (ending,proof_obj)
 
 (* Miscellaneous *)
 
@@ -387,3 +415,13 @@ let get_current_context () =
   try Pfedit.get_current_goal_context ()
   with e when Logic.catchable_exception e ->
     (Evd.empty, Global.env())
+
+
+
+
+
+
+
+
+
+
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
index 25e5a44304..65efff271f 100644
--- a/toplevel/lemmas.mli
+++ b/toplevel/lemmas.mli
@@ -18,7 +18,7 @@ open Pfedit
 (** A hook start_proof calls on the type of the definition being started *)
 val set_start_hook : (types -> unit) -> unit
 
-val start_proof : Id.t -> goal_kind -> types ->
+val start_proof : Id.t -> goal_kind -> ?sign:Environ.named_context_val -> types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
    unit declaration_hook -> unit
 
@@ -31,35 +31,17 @@ val start_proof_with_initialization :
   (Id.t * (types * (Name.t list * Impargs.manual_explicitation list))) list
   -> int list option -> unit declaration_hook -> unit
 
-(** A hook the next three functions pass to cook_proof *)
-val set_save_hook : (Proof.proof -> unit) -> unit
-
 (** {6 ... } *)
-(** [save_named b] saves the current completed (or the provided) proof
-    under the name it was started; boolean [b] tells if the theorem is 
-    declared opaque; it fails if the proof is not completed *)
-
-val save_named : ?proof:Proof_global.closed_proof -> bool -> unit
-
-(** [save_anonymous b name] behaves as [save_named] but declares the theorem
-under the name [name] and respects the strength of the declaration *)
 
-val save_anonymous :
-  ?proof:Proof_global.closed_proof -> bool -> Id.t -> unit
-
-(** [save_anonymous_with_strength s b name] behaves as [save_anonymous] but
-   declares the theorem under the name [name] and gives it the
-   strength [strength] *)
-
-val save_anonymous_with_strength :
-  ?proof:Proof_global.closed_proof -> theorem_kind -> bool -> Id.t -> unit
+(** A hook the next three functions pass to cook_proof *)
+val set_save_hook : (Proof.proof -> unit) -> unit
 
-(** [admit ()] aborts the current goal and save it as an assmumption *)
+val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit
 
-val admit : unit -> unit
 
 (** [get_current_context ()] returns the evar context and env of the
    current open proof if any, otherwise returns the empty evar context
    and the current global env *)
 
 val get_current_context : unit -> Evd.evar_map * Environ.env
+
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index d8f9052563..de0ece06d3 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -1805,7 +1805,7 @@ let show_script ?proof () =
     let prf =
       match proof with
       | None -> Pfedit.get_current_proof_name ()
-      | Some (id,_) -> id in
+      | Some (p,_) -> p.Proof_global.id in
     let cmds = get_script prf in
     let _,_,_,indented_cmds =
       List.fold_left indent_script_item ((1,[]),false,[],[]) cmds
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d5e6ff1907..db51ff6103 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -457,17 +457,10 @@ let qed_display_script = ref true
 let show_script = ref (fun ?proof () -> ())
 
 let vernac_end_proof ?proof = function
-  | Admitted ->
-    admit ();
-    Pp.feedback Interface.AddedAxiom
-  | Proved (is_opaque,idopt) ->
+  | Admitted -> save_proof ?proof Admitted
+  | Proved (_,_) as e ->
     if is_verbose () && !qed_display_script then !show_script ?proof ();
-    begin match idopt with
-    | None -> save_named ?proof is_opaque
-    | Some ((_,id),None) -> save_anonymous ?proof is_opaque id
-    | Some ((_,id),Some kind) -> 
-        save_anonymous_with_strength ?proof kind is_opaque id
-    end
+    save_proof ?proof e
 
   (* A stupid macro that should be replaced by ``Exact c. Save.'' all along
      the theories [??] *)
@@ -476,7 +469,7 @@ let vernac_exact_proof c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the begining of a proof. *)
   let status = by (Tactics.New.exact_proof c) in
-  save_named true;
+  save_proof (Vernacexpr.Proved(true,None));
   if not status then Pp.feedback Interface.AddedAxiom
 
 let vernac_assumption locality (local, kind) l nl =