From 9bb1b959071575074870ba2a11ca79cb52cb7e8b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 20 Dec 2013 17:51:24 +0100
Subject: STM: set loc for aux file when interpreting vernac

---
 toplevel/stm.ml | 1 +
 1 file changed, 1 insertion(+)

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))
-- 
cgit v1.2.3