diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-21 21:20:50 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:58:32 +0100 |
commit | 81f14b203ac8476623ed6567844df452a1646a60 (patch) | |
tree | fd4cac9ab6aa83c52f01e7c523b80f0dc9593426 /test-suite/failure/ltac4.v | |
parent | 00191b7dea128e21abcde02cc45b02d23c205595 (diff) |
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.
Diffstat (limited to 'test-suite/failure/ltac4.v')
0 files changed, 0 insertions, 0 deletions