From 9a6687294866bc9fb6f9f3fd37842b59668f85b1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 3 Jul 2019 13:33:42 +0200
Subject: [vernac] Fix bad merge which resulted in wrong module name.

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

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 793ba72fd3..681605cc31 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2684,7 +2684,7 @@ and interp_control ?proof ~st v = match v with
     let before_univs = Global.universes () in
     let pstack = interp_expr ?proof ~atts ~st cmd in
     if before_univs == Global.universes () then pstack
-    else Option.map (Lemmas.Stack.map_top_pstate ~f:Proof_global.update_global_env) pstack
+    else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack
   | { v=VernacFail v } ->
     with_fail ~st (fun () -> interp_control ?proof ~st v);
     st.Vernacstate.lemmas
-- 
cgit v1.2.3