diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/derive/derive.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/CHANGES | 4 | ||||
| -rw-r--r-- | plugins/extraction/haskell.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 |
8 files changed, 22 insertions, 7 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 1524079f42..6d3d4b7432 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/extraction/CHANGES b/plugins/extraction/CHANGES index cf97ae3ab8..4bc3dba36e 100644 --- a/plugins/extraction/CHANGES +++ b/plugins/extraction/CHANGES @@ -54,7 +54,7 @@ but also a few steps toward a more user-friendly extraction: * bug fixes: - many concerning Records. -- a Stack Overflow with mutual inductive (PR#320) +- a Stack Overflow with mutual inductive (BZ#320) - some optimizations have been removed since they were not type-safe: For example if e has type: type 'x a = A Then: match e with A -> A -----X----> e @@ -125,7 +125,7 @@ but also a few steps toward a more user-friendly extraction: - the dummy constant "__" have changed. see README - - a few bug-fixes (#191 and others) + - a few bug-fixes (BZ#191 and others) 7.2 -> 7.3 diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 0f537abece..f708307c38 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -145,7 +145,7 @@ let rec pp_expr par env args = | MLrel n -> let id = get_db_name n env in (* Try to survive to the occurrence of a Dummy rel. - TODO: we should get rid of this hack (cf. #592) *) + TODO: we should get rid of this hack (cf. BZ#592) *) let id = if Id.equal id dummy_name then Id.of_string "__" else id in apply (Id.print id) | MLapp (f,args') -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 1e8854249a..76fcd5ec87 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 2e2ced790e..d41abee87e 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 2997537664..9cb2a0a3f5 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 74c454334e..76f859ed72 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 bcd5b388a1..0bf6e3d155 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; |