From e3e257dd35b14420c0ca1aea801200f857c6394e Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 19 Dec 2013 11:18:45 +0100
Subject: Remove obsolete comment about Let being processed synchronously

Let proof terms are stocked in the named_context that is used directly
everywhere, hence there is no way to stock a Future proof term there.
---
 kernel/safe_typing.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ebfb99c73e..66bc907897 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -282,7 +282,6 @@ let safe_push_named (id,_,_ as d) env =
 
 let push_named_def (id,de) senv =
   let (c,typ,cst) = Term_typing.translate_local_def senv.env id de in
-  (* XXX for now we force *)
   let c = match c with
     | Def c -> Lazyconstr.force c
     | OpaqueDef c -> Lazyconstr.force_opaque (Future.join c)
-- 
cgit v1.2.3