aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/prettyp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/prettyp.ml')
-rw-r--r--printing/prettyp.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index da230ee0d..031db5b0c 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -531,11 +531,11 @@ 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 (Opaqueproof.force_proof lc)
| Def c ->
str "Definition " ++ print_basename con ++ cut () ++
str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++
- pr_lconstr (Lazyconstr.force c))
+ pr_lconstr (Mod_subst.force_constr c))
++ str "." ++ fnl () ++ fnl ()
| "INDUCTIVE" ->
let mind = Global.mind_of_delta_kn kn in