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
---
 kernel/modops.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'kernel/modops.ml')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 986118655e..c1b5d788d3 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -20,6 +20,7 @@ open Util
 open Names
 open Term
 open Declarations
+open Declareops
 open Environ
 open Entries
 open Mod_subst
@@ -287,7 +288,7 @@ let strengthen_const mp_from l cb resolver =
       let kn = KerName.make2 mp_from l in
       let con = constant_of_delta_kn resolver kn in
       { cb with
-	const_body = Def (Declarations.from_val (mkConst con));
+	const_body = Def (Lazyconstr.from_val (mkConst con));
 	const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con)
       }
 
@@ -377,7 +378,7 @@ let inline_delta_resolver env inl mp mbid mtb delta =
 	  match constant.const_body with
 	    | Undef _ | OpaqueDef _ -> l
 	    | Def body ->
-	      let constr = Declarations.force body in
+	      let constr = Lazyconstr.force body in
 	      add_inline_delta_resolver kn (lev, Some constr) l
 	with Not_found ->
 	  error_no_such_label_sub (con_label con)
-- 
cgit v1.2.3