diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index bc77424c5..8cbc8312e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -90,7 +90,8 @@ let show_proof () = msgnl (str"LOC: " ++ prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++ str"Subgoals" ++ fnl () ++ - prlist (fun (mv,ty) -> int mv ++ str" -> " ++ prtype ty ++ fnl ()) + prlist (fun (mv,ty) -> Nameops.pr_meta mv ++ str" -> " ++ + prtype ty ++ fnl ()) meta_types ++ str"Proof: " ++ prterm (Evarutil.nf_evar evc pfterm)) |