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, 67 insertions, 46 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 8a52244df..e4cdf4989 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 6dad738af..110df2347 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 b7a32a980..b2282a683 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 e88c2f394..eb7d0ecb1 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 *)