diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 9a084adc48..0f6a5e8937 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -420,11 +420,11 @@ let print_constant with_values sep sp = str"*** [ " ++ print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ - Printer.pr_univ_cstr cb.const_constraints + Printer.pr_univ_cstr (Future.force cb.const_constraints) | _ -> print_basename sp ++ str sep ++ cut () ++ (if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++ - Printer.pr_univ_cstr cb.const_constraints) + Printer.pr_univ_cstr (Future.force cb.const_constraints)) let gallina_print_constant_with_infos sp = print_constant true " = " sp ++ @@ -566,7 +566,8 @@ let print_full_pure_context () = | OpaqueDef lc -> str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr (Lazyconstr.force_opaque lc) + str "Proof " ++ pr_lconstr + (Lazyconstr.force_opaque (Future.force lc)) | Def c -> str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++ |