Merge PR #9645: [proof] Remove terminator type, unifying regular and obligation ones.

Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot

2 files changed, 11 insertions, 8 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index bddea41145..0b1a7fcc03 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -24,9 +24,6 @@ module NamedDecl = Context.Named.Declaration
 
 (*** Proof Global Environment ***)
 
-(* Extra info on proofs. *)
-type lemma_possible_guards = int list list
-
 type proof_object = {
   id : Names.Id.t;
   entries : Evd.side_effects Entries.definition_entry list;
@@ -264,14 +261,22 @@ let return_proof ?(allow_partial=false) ps =
   let evd = Proof.return ~pid proof in
   let eff = Evd.eval_side_effects evd in
   let evd = Evd.minimize_universes evd in
-  (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
-     side-effects... This may explain why one need to uniquize side-effects
-     thereafter... *)
   let proof_opt c =
     match EConstr.to_constr_opt evd c with
     | Some p -> p
     | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
   in
+  (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+     side-effects... This may explain why one need to uniquize side-effects
+     thereafter... *)
+  (* EJGA: actually side-effects de-duplication and this codepath is
+     unrelated. Duplicated side-effects arise from incorrect scheme
+     generation code, the main bulk of it was mostly fixed by #9836
+     but duplication can still happen because of rewriting schemes I
+     think; however the code below is mostly untested, the only
+     code-paths that generate several proof entries are derive and
+     equations and so far there is no code in the CI that will
+     actually call those and do a side-effect, TTBOMK *)
   let proofs =
     List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in
     proofs, Evd.evar_universe_context evd
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 162f02b654..15685bd9b6 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -31,8 +31,6 @@ val compact_the_proof : t -> t
     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 : Evd.side_effects Entries.definition_entry list;