diff options
| author | Enrico Tassi | 2014-10-13 15:06:44 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-10-13 18:13:21 +0200 |
| commit | d24e6d915d0170d5d3e9690c053a0b0b4c2758e5 (patch) | |
| tree | 005f235728e21fb65e27b1c49c90f10b933495a6 /kernel/nativecode.ml | |
| parent | 0253fc47be156d0d87cccda32c5bb90bc37960da (diff) | |
Stm: more precise representation of nested proofs
This fixes the bug reported by Hugo:
2) Goal True.
3-4) Definition a:=0.
5) Goal True True.
(* jumped back to 3 (on master) instead of 4 (on the outermost proof) *)
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions