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.

1 files changed, 0 insertions, 5 deletions

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 ();