diff options
| author | gareuselesinge | 2013-10-18 13:52:10 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-10-18 13:52:10 +0000 |
| commit | 020aa7a8e9bca88631e6d7fa68d1ff462f5af25a (patch) | |
| tree | fbd29a9da01f1de8b290547fd64596a56ef83aed /kernel/term_typing.ml | |
| parent | 27bbbdc0ef930b1efca7b268e859d4e93927b365 (diff) | |
Future: ported to Ephemeron + exception enhancing
A future always carries a fix_exn with it: a function that enriches
an exception with the state in which the error occurs and also a safe
state close to it where one could backtrack.
A future can be in two states: Ongoing or Finished.
The latter state is obtained by Future.join and after that the future
can be safely marshalled.
An Ongoing future can be marshalled, but its value is lost. This makes
it possible to send the environment to a slave process without
pre-processing it to drop all unfinished proofs (they are dropped
automatically in some sense).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16892 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 567511c93f..987621619a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -84,9 +84,8 @@ let infer_declaration ?(what="UNKNOWN") env dcl = | DefinitionEntry c -> let ctx, entry_body = c.const_entry_secctx, c.const_entry_body in if c.const_entry_opaque && not (Option.is_empty c.const_entry_type) then - let id = "infer_declaration " ^ what in let body_cst = - Future.chain ~id entry_body (fun (body, side_eff) -> + Future.chain entry_body (fun (body, side_eff) -> let body = handle_side_effects env body side_eff in let j, cst = infer env body in let j = @@ -163,7 +162,7 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) = check declared inferred; x | OpaqueDef lc -> (* In this case we can postpone the check *) - OpaqueDef (Future.chain ~id:(string_of_con kn) lc (fun lc -> + OpaqueDef (Future.chain lc (fun lc -> let ids_typ = global_vars_set_constant_type env typ in let ids_def = global_vars_set env (Lazyconstr.force_opaque lc) in @@ -198,7 +197,7 @@ let translate_local_def env id centry = let translate_mind env kn mie = Indtypes.check_inductive env kn mie let handle_side_effects env ce = { ce with - const_entry_body = Future.chain ~id:"handle_side_effects" + const_entry_body = Future.chain ce.const_entry_body (fun (body, side_eff) -> - handle_side_effects env body side_eff, Declareops.no_seff); + handle_side_effects env body side_eff, Declareops.no_seff); } |