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.

4 files changed, 83 insertions, 70 deletions

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 =