aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/vernacentries.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/vernacentries.ml')
-rw-r--r--vernac/vernacentries.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5eae4fd7f..4c9b41b21 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -66,8 +66,8 @@ let show_proof () =
let show_top_evars () =
(* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
let pfts = Proof_global.give_me_the_proof () in
- let gls,_,_,_,sigma = Proof.proof pfts in
- pr_evars_int sigma 1 (Evd.undefined_map sigma)
+ let gls,_,shelf,givenup,sigma = Proof.proof pfts in
+ pr_evars_int sigma ~shelf ~givenup 1 (Evd.undefined_map sigma)
let show_universes () =
let pfts = Proof_global.give_me_the_proof () in