From 9243166490e8c939bbf6aa0316e99025b25e6398 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 20 Nov 2017 18:17:58 +0100
Subject: [vernac] Adjust `interp` to pass polymorphic in the attributes.

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

(limited to 'stm/stm.ml')

diff --git a/stm/stm.ml b/stm/stm.ml
index 0ee9ea084..ab44cc98b 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1023,7 +1023,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t
   | VernacShow ShowScript -> ShowScript.show_script (); st
   | expr ->
     stm_pperr_endline Pp.(fun () -> str "interpreting " ++ Ppvernac.pr_vernac expr);
-    try Vernacentries.interp ?verbosely:(Some verbose) ?proof st (Loc.tag ?loc expr)
+    try Vernacentries.interp ?verbosely:(Some verbose) ?proof ~st (Loc.tag ?loc expr)
     with e ->
       let e = CErrors.push e in
       Exninfo.iraise Hooks.(call_process_error_once e)
-- 
cgit v1.2.3