diff options
| author | Enrico Tassi | 2013-12-20 17:51:24 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-01-04 17:07:15 +0100 |
| commit | 9bb1b959071575074870ba2a11ca79cb52cb7e8b (patch) | |
| tree | 9cf81621b195fa06c3ac68e2a58a63099840fb70 | |
| parent | ba2d8da59c9502bb892179223b4b2f39a41c09c2 (diff) | |
STM: set loc for aux file when interpreting vernac
| -rw-r--r-- | toplevel/stm.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 2f616603b9..b3dcc4bf60 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -40,6 +40,7 @@ let vernac_interp ?proof id (verbosely, loc, expr) = prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr)) end else begin Pp.set_id_for_feedback (Interface.State id); + Aux_file.record_in_aux_set_at loc; prerr_endline ("interpreting " ^ string_of_ppcmds(pr_vernac expr)); try Vernacentries.interp ~verbosely ?proof (loc, expr) with e -> raise (Errors.push (Cerrors.process_vernac_interp_error e)) |