diff options
| author | Shachar Itzhaky | 2019-04-11 13:58:28 +0300 |
|---|---|---|
| committer | Shachar Itzhaky | 2019-04-11 14:01:22 +0300 |
| commit | df70c87cd7adab8a748a248f7660738dcc043186 (patch) | |
| tree | c9f4b7026ef309cb8c6a2072c0dd2bded1c026ca /stm | |
| parent | 36c15766a9295d980d142da0e42aebf1309f4eb4 (diff) | |
[stm] Report correct ids on some errors where it was dummy.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index d54a5fdf43..e1ab45163a 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2970,7 +2970,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on." |> Pp.str |> (fun s -> (UserError (None, s), Exninfo.null)) - |> State.exn_on ~valid:Stateid.dummy Stateid.dummy + |> State.exn_on ~valid:Stateid.dummy newtip |> Exninfo.iraise else @@ -3054,7 +3054,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) "Commands which may open proofs are not allowed in a proof unless you turn option Nested Proofs Allowed on." |> Pp.str |> (fun s -> (UserError (None, s), Exninfo.null)) - |> State.exn_on ~valid:Stateid.dummy Stateid.dummy + |> State.exn_on ~valid:Stateid.dummy newtip |> Exninfo.iraise else let id = VCS.new_node ~id:newtip proof_mode () in |