diff options
| author | Arnaud Spiwack | 2014-07-23 15:16:18 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-07-23 17:43:18 +0200 |
| commit | e143cffaeab1a294ca08a49443747c66bc963c29 (patch) | |
| tree | 604425df88d5cb36916d562b67b9426c7d30bd0d /plugins | |
| parent | 474197250baa3366385563bc5403a0871d106275 (diff) | |
When closing a proof, make sure that the types have their evar substituted.
When starting proofs with [start_dependent_proof], we may have initial goals with existential variables in their conclusion. They will be solved by the proof, but this information was not propagated in close proof, and the kernel failed on uninstanciated evars.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions