Refactoring: storing more information in the terminator closure.

We used to keep a lot of information in the global proof environment, for the end-of-proof commands to use. Now that the end commands are dumb, they are better stored in the proof-termination closure allocated by the starting command.

In this commit, we remove the compute_guard parameter.

6 files changed, 16 insertions, 24 deletions

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index db4297b37..604d7d853 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -166,7 +166,7 @@ let save with_clean id const (locality,kind) hook =
 
 
 let cook_proof _ =
-  let (id,(entry,_,strength,hook)) = Pfedit.cook_proof (fun _ -> ()) in
+  let (id,(entry,strength,hook)) = Pfedit.cook_proof (fun _ -> ()) in
   (id,(entry,strength,hook))
 
 let get_proof_clean do_reduce =
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e4cdf4989..83eb47bb9 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 terminator =
+let start_proof (id : Id.t) str hyps c ?init_tac hook terminator =
   let goals = [ (Global.env_of_context hyps , c) ] in
-  Proof_global.start_proof id str goals ?compute_guard hook terminator;
+  Proof_global.start_proof id str goals hook terminator;
   let env = Global.env () in
   ignore (Proof_global.with_current_proof (fun _ p ->
     match init_tac with
@@ -40,8 +40,8 @@ let start_proof (id : Id.t) str hyps c ?init_tac ?compute_guard hook terminator
 
 let cook_this_proof hook p =
   match p with
-  | { Proof_global.id;entries=[constr];do_guard;persistence;hook } ->
-      (id,(constr,do_guard,persistence,hook))
+  | { Proof_global.id;entries=[constr];persistence;hook } ->
+      (id,(constr,persistence,hook))
   | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
 
 let cook_proof hook =
@@ -126,7 +126,7 @@ let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac
   start_proof id goal_kind sign typ (fun _ _ -> ()) (fun _ -> ());
   try
     let status = by tac in
-    let _,(const,_,_,_) = cook_proof (fun _ -> ()) in
+    let _,(const,_,_) = cook_proof (fun _ -> ()) in
     delete_current_proof ();
     const, status
   with reraise ->
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 110df2347..9762d415f 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -61,7 +61,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 -> 
+  ?init_tac:unit Proofview.tactic ->
   unit declaration_hook -> Proof_global.proof_terminator -> unit
 
 (** {6 ... } *)
@@ -73,12 +73,12 @@ val start_proof :
 val cook_this_proof : (Proof.proof -> unit) ->
     Proof_global.proof_object ->
   (Id.t *
-    (Entries.definition_entry * lemma_possible_guards * goal_kind *
+    (Entries.definition_entry * goal_kind *
      unit declaration_hook Ephemeron.key))
 
 val cook_proof : (Proof.proof -> unit) ->
   (Id.t *
-    (Entries.definition_entry * lemma_possible_guards * goal_kind *
+    (Entries.definition_entry * goal_kind *
      unit declaration_hook Ephemeron.key))
 
 (** {6 ... } *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index b2282a683..2534a1ec7 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -68,7 +68,6 @@ 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
 }
@@ -85,7 +84,6 @@ type pstate = {
   section_vars : Context.section_context option;
   proof : Proof.proof;
   strength : Decl_kinds.goal_kind;
-  compute_guard : lemma_possible_guards;
   pr_hook : unit Tacexpr.declaration_hook Ephemeron.key;
   mode : proof_mode Ephemeron.key;
 }
@@ -250,7 +248,7 @@ end
     It raises exception [ProofInProgress] if there is a proof being
     currently edited. *)
 
-let start_proof id str goals ?(compute_guard=[]) hook terminator =
+let start_proof id str goals hook terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
@@ -258,12 +256,11 @@ let start_proof id str goals ?(compute_guard=[]) hook terminator =
     endline_tactic = None;
     section_vars = None;
     strength = str;
-    compute_guard = compute_guard;
     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 terminator =
+let start_dependent_proof id str goals hook terminator =
   let initial_state = {
     pid = id;
     terminator = Ephemeron.create terminator;
@@ -271,7 +268,6 @@ let start_dependent_proof id str goals ?(compute_guard=[]) hook terminator =
     endline_tactic = None;
     section_vars = None;
     strength = str;
-    compute_guard = compute_guard;
     pr_hook = Ephemeron.create hook;
     mode = find_proof_mode "No" } in
   push initial_state pstates
@@ -297,7 +293,7 @@ let get_open_goals () =
   List.length shelf
 
 let close_proof ~now fpl =
-  let { pid;section_vars;compute_guard;strength;pr_hook;proof;terminator } =
+  let { pid;section_vars;strength;pr_hook;proof;terminator } =
     cur_pstate ()
   in
   let initial_goals = Proof.initial_goals proof in
@@ -311,7 +307,6 @@ let close_proof ~now fpl =
     List.iter (fun x -> ignore(Future.join x.Entries.const_entry_body)) entries;
   { id = pid ;
     entries = entries ;
-    do_guard = compute_guard ;
     persistence = strength ;
     hook = pr_hook } , terminator
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index eb7d0ecb1..71d03438b 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -56,7 +56,6 @@ 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
 }
@@ -74,7 +73,6 @@ type closed_proof = proof_object*proof_terminator Ephemeron.key
 val start_proof : Names.Id.t ->
                           Decl_kinds.goal_kind ->
                           (Environ.env * Term.types) list  ->
-                          ?compute_guard:lemma_possible_guards ->
                           unit Tacexpr.declaration_hook ->
                           proof_terminator ->
                           unit
@@ -83,7 +81,6 @@ val start_proof : Names.Id.t ->
 val start_dependent_proof : Names.Id.t ->
                           Decl_kinds.goal_kind ->
                           Proofview.telescope  ->
-                          ?compute_guard:lemma_possible_guards ->
                           unit Tacexpr.declaration_hook ->
                           proof_terminator ->
                           unit
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index db479615e..9d7a58ff0 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -299,8 +299,8 @@ let start_hook = ref ignore
 let set_start_hook = (:=) start_hook
 
 
-let get_proof proof opacity =
-  let (id,(const,do_guard,persistence,hook)) =
+let get_proof proof do_guard opacity =
+  let (id,(const,persistence,hook)) =
     Pfedit.cook_this_proof !save_hook proof
   in
   id,{const with const_entry_opaque = opacity},do_guard,persistence,hook
@@ -311,7 +311,7 @@ let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook =
         admit ();
         Pp.feedback Interface.AddedAxiom
     | Proved (is_opaque,idopt),proof ->
-        let proof = get_proof proof is_opaque in
+        let proof = get_proof proof compute_guard is_opaque in
         begin match idopt with
         | None -> save_named proof
         | Some ((_,id),None) -> save_anonymous proof id
@@ -325,7 +325,7 @@ let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook =
     | None -> initialize_named_context_for_proof ()
   in
   !start_hook c;
-  Pfedit.start_proof id kind sign c ?init_tac ~compute_guard hook terminator
+  Pfedit.start_proof id kind sign c ?init_tac hook terminator
 
 
 let rec_tac_initializer finite guard thms snl =