diff options
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 68c2ed328..f45eb2a3a 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -126,6 +126,7 @@ let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac delete_current_proof (); const, status with reraise -> + let reraise = Errors.push reraise in delete_current_proof (); raise reraise |