From 1e485645ef6481a856e8a67477f186519fb8ec9d Mon Sep 17 00:00:00 2001
From: coq
Date: Sat, 5 Oct 2002 11:03:20 +0000
Subject: Lazy experimentale temporaire...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/declarations.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 05989bc82a..d3c7681c09 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -23,7 +23,7 @@ open Sign
 
 type constant_body = {
   const_hyps : section_context; (* New: younger hyp at top *)
-  const_body : constr option;
+  const_body : constr Lazy.t option;
   const_type : types;
   const_constraints : constraints;
   const_opaque : bool }
@@ -88,9 +88,12 @@ type mutual_inductive_body = {
   mind_equiv : kernel_name option
  }
 
+let lazy_subst sub l_constr = 
+  lazy (subst_mps sub (Lazy.force_val l_constr))
+
 (* TODO: should be changed to non-coping after Term.subst_mps *)
 let subst_const_body sub cb = 
-  { const_body = option_app (Term.subst_mps sub) cb.const_body;
+  { const_body = option_app (lazy_subst sub) cb.const_body;
     const_type = type_app (Term.subst_mps sub) cb.const_type;
     const_hyps = (assert (cb.const_hyps=[]); []);
     const_constraints = cb.const_constraints;
-- 
cgit v1.2.3