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/nativelambda.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'kernel/nativelambda.ml')

diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index f530f6e2ec..9c400e4c03 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -631,11 +631,13 @@ and lambda_of_app env f args =
       let cb = lookup_constant kn !global_env in
       begin match cb.const_body with
       | Def csubst ->
-          if cb.const_inline_code then lambda_of_app env (force csubst) args
+          if cb.const_inline_code then
+            lambda_of_app env (Lazyconstr.force csubst) args
           else
           let prefix = get_const_prefix !global_env kn in
           let t =
-            if is_lazy (force csubst) then mkLapp Lforce [|Lconst (prefix, kn)|]
+            if is_lazy (Lazyconstr.force csubst) then
+              mkLapp Lforce [|Lconst (prefix, kn)|]
             else Lconst (prefix, kn)
           in
         mkLapp t (lambda_of_args env 0 args)
-- 
cgit v1.2.3