diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2013-12-19 11:18:45 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-04 17:07:15 +0100 |
| commit | e3e257dd35b14420c0ca1aea801200f857c6394e (patch) | |
| tree | d45534a93121ba9d58e0617f1c5648dd61502716 /kernel/safe_typing.ml | |
| parent | fd57985d7f6e9be8f5ec556f5b091f7b9f6d9848 (diff) | |
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.
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ebfb99c73..66bc90789 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) |