diff options
| author | Emilio Jesus Gallego Arias | 2019-08-14 18:21:10 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-14 21:19:04 +0200 |
| commit | f10cc5bbadf94210cc2ddc3835cc09228d71bde7 (patch) | |
| tree | d50a38530e7e77b984c3640a1c7b7ccad4b19110 /stm | |
| parent | d2bf9204b83682f0da579fc3accf35125e55c302 (diff) | |
[vernac] Refactor common parts of interp_{,delayed}
This should fix some bugs w.r.t. management of state introduced in
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 17cef26997..7f0632bd7c 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1056,7 +1056,7 @@ end (* }}} *) (* Wrapper for the proof-closing special path for Qed *) let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc ~control pending : Vernacstate.t = set_id_for_feedback ?route dummy_doc id; - Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ?loc:loc ~control pending + Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ~control (CAst.make ?loc pending) (* Wrapper for Vernacentries.interp to set the feedback id *) (* It is currently called 19 times, this number should be certainly |