From f10cc5bbadf94210cc2ddc3835cc09228d71bde7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 14 Aug 2019 18:21:10 +0200
Subject: [vernac] Refactor common parts of interp_{,delayed}

This should fix some bugs w.r.t. management of state introduced in
---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

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