diff options
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |