diff options
| -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)) |
