diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-06-02 10:52:31 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-06-08 11:17:05 +0200 |
| commit | 289b2b9a1c3d3ebc3c1975663d16c04e88b6329b (patch) | |
| tree | b8484b831d9fe3d027c186ebe86acbc82426fea3 /theories/Bool | |
| parent | e1ba72037191b1d4be9de8a0a8fc1faa24eeb12c (diff) | |
Enforce a correct exception handling in declaration_hooks
This should finally get rid of the following class of bugs:
Qed fails, STM undoes to the beginning of the proof because the
exception is not annotated with the correct state, PG gets out of
sync because errors always refer to the last command in PGIP.
Diffstat (limited to 'theories/Bool')
0 files changed, 0 insertions, 0 deletions