diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 11 | ||||
| -rw-r--r-- | tactics/equality.mli | 4 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 9 | ||||
| -rw-r--r-- | tactics/tactics.ml | 21 |
4 files changed, 17 insertions, 28 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 26ae35a79d..8478c1957a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1651,17 +1651,6 @@ let cutSubstClause l2r eqn cls = | None -> cutSubstInConcl l2r eqn | Some id -> cutSubstInHyp l2r eqn id -let warn_deprecated_cutrewrite = - CWarnings.create ~name:"deprecated-cutrewrite" ~category:"deprecated" - (fun () -> strbrk"\"cutrewrite\" is deprecated. Use \"replace\" instead.") - -let cutRewriteClause l2r eqn cls = - warn_deprecated_cutrewrite (); - try_rewrite (cutSubstClause l2r eqn cls) - -let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id) -let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None - let substClause l2r c cls = Proofview.Goal.enter begin fun gl -> let eq = pf_apply get_type_of gl c in diff --git a/tactics/equality.mli b/tactics/equality.mli index fdcbbc0e3c..5a4fe47cab 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -107,10 +107,6 @@ val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr - val make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr) -(* The family cutRewriteIn expect an equality statement *) -val cutRewriteInHyp : bool -> types -> Id.t -> unit Proofview.tactic -val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic - (* The family rewriteIn expect the proof of an equality *) val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic val rewriteInConcl : bool -> constr -> unit Proofview.tactic diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index fc099f643d..c0fad0026f 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -695,6 +695,8 @@ module New = struct (* Check that holes in arguments have been resolved *) let check_evars env sigma extsigma origsigma = + let reachable = lazy (Evarutil.reachable_from_evars sigma + (Evar.Map.domain (Evd.undefined_map origsigma))) in let rec is_undefined_up_to_restriction sigma evk = if Evd.mem origsigma evk then None else let evi = Evd.find sigma evk in @@ -710,7 +712,12 @@ module New = struct let rest = Evd.fold_undefined (fun evk evi acc -> match is_undefined_up_to_restriction sigma evk with - | Some (evk',evi) -> (evk',evi)::acc + | Some (evk',evi) -> + (* If [evk'] descends from [evk] which descends itself from + an originally undefined evar in [origsigma], it is a not + a fresh undefined hole from [sigma]. *) + if Evar.Set.mem evk (Lazy.force reachable) then acc + else (evk',evi)::acc | _ -> acc) extsigma [] in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5f7e35d205..686779b1d2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3248,13 +3248,10 @@ let rec consume_pattern avoid na isdep gl = let open CAst in function | {loc;v=IntroForthcoming true}::names when not isdep -> consume_pattern avoid na isdep gl names | {loc;v=IntroForthcoming _}::names as fullpat -> - let avoid = Id.Set.union avoid (explicit_intro_names names) in (CAst.make ?loc @@ intropattern_of_name gl avoid na, fullpat) | {loc;v=IntroNaming IntroAnonymous}::names -> - let avoid = Id.Set.union avoid (explicit_intro_names names) in (CAst.make ?loc @@ intropattern_of_name gl avoid na, names) | {loc;v=IntroNaming (IntroFresh id')}::names -> - let avoid = Id.Set.union avoid (explicit_intro_names names) in (CAst.make ?loc @@ IntroNaming (IntroIdentifier (new_fresh_id avoid id' gl)), names) | pat::names -> (pat,names) @@ -3312,7 +3309,7 @@ let get_recarg_dest (recargdests,tophyp) = *) let induct_discharge with_evars dests avoid' tac (avoid,ra) names = - let avoid = Id.Set.union avoid avoid' in + let avoid = Id.Set.union avoid' (Id.Set.union avoid (explicit_intro_names names)) in let rec peel_tac ra dests names thin = match ra with | (RecArg,_,deprec,recvarname) :: @@ -3320,7 +3317,7 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names = Proofview.Goal.enter begin fun gl -> let (recpat,names) = match names with | [{CAst.loc;v=IntroNaming (IntroIdentifier id)} as pat] -> - let id' = next_ident_away (add_prefix "IH" id) avoid in + let id' = new_fresh_id avoid (add_prefix "IH" id) gl in (pat, [CAst.make @@ IntroNaming (IntroIdentifier id')]) | _ -> consume_pattern avoid (Name recvarname) deprec gl names in let dest = get_recarg_dest dests in @@ -5184,14 +5181,14 @@ end (** Tacticals defined directly in term of Proofview *) module New = struct - open Genredexpr - open Locus - let reduce_after_refine = - reduce - (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true; - rZeta=false;rDelta=false;rConst=[]}) - {onhyps = Some []; concl_occs = AllOccurrences } + (* For backward compatibility reasons, we do not contract let-ins, but we unfold them. *) + let redfun env t = + let open CClosure in + let flags = RedFlags.red_add_transparent allnolet TransparentState.empty in + clos_norm_flags flags env t + in + reduct_in_concl ~check:false (redfun,DEFAULTcast) let refine ~typecheck c = Refine.refine ~typecheck c <*> |