From 15b6c9b6fa268a9af6dd4f05961e469545e92a6f Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 24 Feb 2014 20:46:32 +0100
Subject: Lazyconstr -> Opaqueproof

Make this module deal only with opaque proofs.
Make discharging/substitution invariant more explicit via a third constructor.
---
 kernel/nativecode.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 7d542c1073..99513319b7 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1523,7 +1523,7 @@ and compile_named env sigma auxdefs id =
 let compile_constant env sigma prefix ~interactive con body =
   match body with
   | Def t ->
-      let t = Lazyconstr.force t in
+      let t = Mod_subst.force_constr t in
       let code = lambda_of_constr env sigma t in
       let is_lazy = is_lazy t in
       let code = if is_lazy then mk_lazy code else code in
@@ -1628,7 +1628,7 @@ let rec compile_deps env sigma prefix ~interactive init t =
       else
       let comp_stack, (mind_updates, const_updates) = match cb.const_body with
         | Def t ->
-	   compile_deps env sigma prefix ~interactive init (Lazyconstr.force t)
+	   compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t)
         | _ -> init
       in
       let code, name =
-- 
cgit v1.2.3