From 60de53d159c85b8300226a61aa502a7e0dd2f04b Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 26 Feb 2013 18:52:24 +0000
Subject: 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
---
 dev/printers.mllib  | 3 ++-
 dev/top_printers.ml | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 0b6ec899e9..7db5b5cb99 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -47,7 +47,8 @@ Cbytecodes
 Copcodes
 Cemitcodes
 Nativevalues
-Declarations
+Lazyconstr
+Declareops
 Retroknowledge
 Pre_env
 Nativelambda
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 0dc09f9baf..db895fc0f7 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -49,7 +49,7 @@ let rawdebug = ref false
 let ppconstr x = pp (Termops.print_constr x)
 let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr x)
 let ppterm = ppconstr
-let ppsconstr x = ppconstr (Declarations.force x)
+let ppsconstr x = ppconstr (Lazyconstr.force x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
 let ppglob_constr = (fun x -> pp(pr_lglob_constr x))
 let pppattern = (fun x -> pp(pr_constr_pattern x))
-- 
cgit v1.2.3