From 81f14b203ac8476623ed6567844df452a1646a60 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 21 Feb 2018 21:20:50 +0100 Subject: Add an invariant on future goals in Proof.run_tactic. More precisely, we check that future goals retrieved in run_tactic have no given_up goals since given_up goals are supposed to be produced only by Proofview.given_up and put on the given_up store. Doing the same for the shelf does not work: there is a situation where run_tactic ends where the same goal is both in the comb and on the shelf. This is when calling "clear x" on a goal "x:A |- ?p:B(?q[x])" when the dependent goal "x:A |- ?q:C" is not on the shelf. Tactic "clear" creates "|- ?p':B(?q'[])" and "|- ?q':C". The "advance" thing sees that the new comb is now composed of ?p' and ?q' but ?q' is a future goal which is later collected on the shelf (which ?q' is also in the comb). I tried to remove this redundancy but apparently it is necessary. There is an example in HoTT (file Classes/theory/rational.v) which requires this redundancy. I did not investigate why: the dependent evar is created by ring as part of a big term. So, as a conclusion, I kept the redundancy. --- proofs/proof.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'proofs/proof.ml') diff --git a/proofs/proof.ml b/proofs/proof.ml index 24f570f01..51e0a1d61 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -347,7 +347,11 @@ let run_tactic env tac pr = Proofview.tclEVARMAP >>= fun sigma -> (* Already solved goals are not to be counted as shelved. Nor are they to be marked as unresolvable. *) - let retrieved = undef sigma (List.rev (Evd.future_goals sigma)) in + let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) (Evd.save_future_goals sigma) in + let retrieved,retrieved_given_up = Evd.extract_given_up_future_goals retrieved in + (* Check that retrieved given up is empty *) + if not (List.is_empty retrieved_given_up) then + CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up."); let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in Proofview.Unsafe.tclEVARS sigma >>= fun () -> Proofview.tclUNIT retrieved -- cgit v1.2.3