diff options
Diffstat (limited to 'proofs/proof_trees.ml')
| -rw-r--r-- | proofs/proof_trees.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index a02ee4faef..a9c65d50c4 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -318,7 +318,8 @@ let pr_seq evd = let pc = pr_ctxt info in let pdcl = prlist_with_sep pr_spc - (fun (id,ty) -> hOV 0 [< print_id id; 'sTR" : ";prterm ty.body >]) + (fun (id,ty) -> + hOV 0 [< print_id id; 'sTR" : ";prterm (body_of_type ty) >]) sign in let pcl = prterm_env_at_top (gLOB hyps) cl in |