aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/printmod.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-02-26 18:52:24 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-02-26 18:52:24 +0000
commit60de53d159c85b8300226a61aa502a7e0dd2f04b (patch)
treee542ed90d58872a75816d451ae26e38fa7b1d9f9 /printing/printmod.ml
parent7dd28b4772251af6ae3641ec63a8251153915e21 (diff)
kernel/declarations becomes a pure mli
- constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml - the functions that were in declarations.ml (mostly substitution utilities and hashcons) are now in kernel/declareops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing/printmod.ml')
-rw-r--r--printing/printmod.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 07a5d954c..57d990b86 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -120,7 +120,7 @@ let print_body is_impl env mp (l,body) =
| Def l when is_impl ->
spc () ++
hov 2 (str ":= " ++
- Printer.pr_lconstr_env env (Declarations.force l))
+ Printer.pr_lconstr_env env (Lazyconstr.force l))
| _ -> mt ()) ++
str ".")
| SFBmind mib ->