diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/derive/derive.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 9 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 2 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 3 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 3 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.ml | 4 |
6 files changed, 19 insertions, 4 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 1524079f4..6d3d4b743 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -10,7 +10,7 @@ open Context.Named.Declaration let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body) : Safe_typing.private_constants Entries.const_entry_body = - Future.chain ~pure:true x begin fun ((b,ctx),fx) -> + Future.chain x begin fun ((b,ctx),fx) -> (f b , ctx) , fx end diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 1e8854249..76fcd5ec8 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -549,3 +549,12 @@ type tcc_lemma_value = | Undefined | Value of Term.constr | Not_needed + +(* We only "purify" on exceptions *) +let funind_purify f x = + let st = Vernacentries.freeze_interp_state `No in + try f x + with e -> + let e = CErrors.push e in + Vernacentries.unfreeze_interp_state st; + Exninfo.iraise e diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 2e2ced790..d41abee87 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -123,3 +123,5 @@ type tcc_lemma_value = | Undefined | Value of Term.constr | Not_needed + +val funind_purify : ('a -> 'b) -> ('a -> 'b) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 299753766..9cb2a0a3f 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -759,7 +759,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let funs = Array.of_list funs and graphs = Array.of_list graphs in let map (c, u) = mkConstU (c, EInstance.make u) in let funs_constr = Array.map map funs in - States.with_state_protection_on_exception + (* XXX STATE Why do we need this... why is the toplevel protection not enought *) + funind_purify (fun () -> let env = Global.env () in let evd = ref (Evd.from_env env) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 74c454334..76f859ed7 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1595,7 +1595,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num spc () ++ str"is defined" ) ) in - States.with_state_protection_on_exception (fun () -> + (* XXX STATE Why do we need this... why is the toplevel protection not enought *) + funind_purify (fun () -> com_terminate tcc_lemma_name tcc_lemma_constr diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index bcd5b388a..0bf6e3d15 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -468,7 +468,9 @@ let register_ltac local tacl = let () = List.iter iter_rec recvars in List.map map rfun in - let defs = Future.transactify defs () in + (* STATE XXX: Review what is going on here. Why does this needs + protection? Why is not the STM level protection enough? Fishy *) + let defs = States.with_state_protection defs () in let iter (def, tac) = match def with | NewTac id -> Tacenv.register_ltac false local id tac; |