diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 19 | ||||
| -rw-r--r-- | plugins/micromega/persistent_cache.ml | 29 |
2 files changed, 24 insertions, 24 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 26e2b18a02..77162ce89a 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -13,7 +13,6 @@ open CErrors open Util open Names open Nameops -open Namegen open Constr open Context open EConstr @@ -485,7 +484,7 @@ let rec decompose_app_rel env evd t = let (f', argl, argr) = decompose_app_rel env evd arg in let ty = Retyping.get_type_of env evd argl in let r = Retyping.relevance_of_type env evd ty in - let f'' = mkLambda (make_annot (Name default_dependent_ident) r, ty, + let f'' = mkLambda (make_annot (Name Namegen.default_dependent_ident) r, ty, mkLambda (make_annot (Name (Id.of_string "y")) r, lift 1 ty, mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |]))) in (f'', argl, argr) @@ -1119,7 +1118,14 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = *) | Lambda (n, t, b) when flags.under_lambdas -> - let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in + let unfresh, n' = + let id = match n.binder_name with + | Anonymous -> Namegen.default_dependent_ident + | Name id -> id + in + let id = Tactics.fresh_id_in_env unfresh id env in + Id.Set.add id unfresh, {n with binder_name = Name id} + in let unfresh = match n'.binder_name with | Anonymous -> unfresh | Name id -> Id.Set.add id unfresh @@ -1542,7 +1548,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = (* For compatibility *) let beta = Tactics.reduct_in_concl ~check:false (Reductionops.nf_betaiota, DEFAULTcast) in let beta_hyp id = Tactics.reduct_in_hyp ~check:false ~reorder:false Reductionops.nf_betaiota (id, InHyp) in - let treat sigma res = + let treat sigma res state = match res with | None -> newfail 0 (str "Nothing to rewrite") | Some None -> @@ -1553,7 +1559,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let (undef, prf, newt) = res in let fold ev _ accu = if Evd.mem sigma ev then accu else ev :: accu in let gls = List.rev (Evd.fold_undefined fold undef []) in - let gls = List.map Proofview.with_empty_state gls in + let gls = List.map (fun gl -> Proofview.goal_with_state gl state) gls in match clause, prf with | Some id, Some p -> let tac = tclTHENLIST [ @@ -1583,6 +1589,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in + let state = Proofview.Goal.state gl in let sigma = Tacmach.New.project gl in let ty = match clause with | None -> concl @@ -1602,7 +1609,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = cl_rewrite_clause_aux ?abs strat env Id.Set.empty sigma ty clause in let sigma = match origsigma with None -> sigma | Some sigma -> sigma in - treat sigma res <*> + treat sigma res state <*> (* For compatibility *) beta <*> Proofview.shelve_unifiable with diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 3360a9a51c..21178a64a5 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -36,10 +36,8 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct module Table = Hashtbl.Make (Key) exception InvalidTableFormat - exception UnboundTable - type mode = Closed | Open - type 'a t = {outch : out_channel; mutable status : mode; htbl : 'a Table.t} + type 'a t = {outch : out_channel; htbl : 'a Table.t} (* XXX: Move to Fun.protect once in Ocaml 4.08 *) let fun_protect ~(finally : unit -> unit) work = @@ -118,7 +116,6 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct close_in_noerr inch; { outch = out_channel_of_descr (openfile f [O_WRONLY; O_APPEND; O_CREAT] 0o666) - ; status = Open ; htbl } with InvalidTableFormat -> (* The file is corrupted *) @@ -131,24 +128,20 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct (fun k e -> Marshal.to_channel outch (k, e) [Marshal.No_sharing]) htbl; flush outch); - {outch; status = Open; htbl} + {outch; htbl} let add t k e = - let {outch; status; htbl = tbl} = t in - if status == Closed then raise UnboundTable - else - let fd = descr_of_out_channel outch in - Table.add tbl k e; - do_under_lock Write fd (fun _ -> - Marshal.to_channel outch (k, e) [Marshal.No_sharing]; - flush outch) + let {outch; htbl = tbl} = t in + let fd = descr_of_out_channel outch in + Table.add tbl k e; + do_under_lock Write fd (fun _ -> + Marshal.to_channel outch (k, e) [Marshal.No_sharing]; + flush outch) let find t k = - let {outch; status; htbl = tbl} = t in - if status == Closed then raise UnboundTable - else - let res = Table.find tbl k in - res + let {outch; htbl = tbl} = t in + let res = Table.find tbl k in + res let memo cache f = let tbl = lazy (try Some (open_in cache) with _ -> None) in |