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.

5 files changed, 10 insertions, 23 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 52ba41869..f4e858903 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 b7072ea3b..db4297b37 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 722f857b3..cea5ffe25 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 0d32bf2bc..7c8f5714e 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 6afbff779..082d7ad51 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"); *)
     );;