diff options
| -rw-r--r-- | kernel/declareops.ml | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 4 | ||||
| -rw-r--r-- | toplevel/command.ml | 2 | ||||
| -rw-r--r-- | toplevel/lemmas.ml | 2 | ||||
| -rw-r--r-- | toplevel/stm.ml | 2 |
6 files changed, 7 insertions, 7 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 8eae2aed8e..724f290926 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -100,7 +100,7 @@ let hcons_const_def = function Def (from_val (Term.hcons_constr constr)) | OpaqueDef lc -> OpaqueDef - (Future.chain ~pure:true lc + (Future.chain ~greedy:true ~pure:true lc (fun lc -> opaque_from_val (Term.hcons_constr (force_opaque lc)))) let hcons_const_body cb = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 35da705efb..ac7a5bb937 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -379,7 +379,7 @@ let add_constant dir l decl senv = (* In coqc, opaque constants outside sections will be stored indirectly in a specific table *) { cb with const_body = - OpaqueDef (Future.chain ~pure:true lc Lazyconstr.turn_indirect) } + OpaqueDef (Future.chain ~greedy:true ~pure:true lc Lazyconstr.turn_indirect) } | _ -> cb in let senv' = add_field (l,SFBconst cb) (C kn) senv in diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 554ed9f9b8..57d4a287b0 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -163,7 +163,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 ~pure:true lc (fun lc -> + OpaqueDef (Future.chain ~greedy:true ~pure:true 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 +198,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 ~pure:true + const_entry_body = Future.chain ~greedy:true ~pure:true ce.const_entry_body (fun (body, side_eff) -> handle_side_effects env body side_eff, Declareops.no_seff); } diff --git a/toplevel/command.ml b/toplevel/command.ml index b2e0e97366..bf226b0bf9 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -69,7 +69,7 @@ let red_constant_entry n ce = function | Some red -> let proof_out = ce.const_entry_body in let env = Global.env () in - { ce with const_entry_body = Future.chain ~pure:true proof_out + { ce with const_entry_body = Future.chain ~greedy:true ~pure:true proof_out (fun (body,eff) -> under_binders env (fst (reduction_of_red_expr env red)) n body,eff) } diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 2adc2feefe..1421aaeed2 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -50,7 +50,7 @@ let adjust_guardness_conditions const = function (* Try all combinations... not optimal *) let env = Global.env() in { const with const_entry_body = - Future.chain ~pure:true const.const_entry_body + Future.chain ~greedy:true ~pure:true const.const_entry_body (fun (body, eff) -> match kind_of_term body with | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 7ea37b08c7..e632d1dbf6 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -540,7 +540,7 @@ end = struct (* {{{ *) let loc = Option.default Loc.ghost (Loc.get_loc e) in let msg = string_of_ppcmds (print e) in Pp.feedback ~state_id:id (Interface.ErrorMsg (loc, msg)); - Stateid.add e ?valid id + Stateid.add (Cerrors.process_vernac_interp_error e) ?valid id let define ?(redefine=false) ?(cache=`No) f id = let str_id = Stateid.to_string id in |