diff options
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 19 |
1 files changed, 13 insertions, 6 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 |