diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 35 | ||||
| -rw-r--r-- | tactics/tactics.ml | 57 |
2 files changed, 52 insertions, 40 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index bc03baf26..cb1d82ae6 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1610,6 +1610,17 @@ user = raise user error specific to rewrite (**********************************************************************) (* Substitutions tactics (JCF) *) +let regular_subst_tactic = ref true + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "more regular behavior of tactic subst"; + optkey = ["Regular";"Subst";"Tactic"]; + optread = (fun () -> !regular_subst_tactic); + optwrite = (:=) regular_subst_tactic } + let restrict_to_eq_and_identity eq = (* compatibility *) if not (is_global glob_eq eq) && not (is_global glob_identity eq) @@ -1638,24 +1649,25 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in (* The set of hypotheses using x *) let dephyps = - List.rev (snd (List.fold_right (fun dcl (deps,allhyps) -> + List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) -> let id = get_id dcl in if not (Id.equal id hyp) && List.exists (fun y -> occur_var_in_decl env y dcl) deps then - ((if is_local_assum dcl then deps else id::deps), id::allhyps) + let id_dest = if !regular_subst_tactic then dest else MoveLast in + (dest,(if is_local_assum dcl then deps else id::deps), (id_dest,id)::allhyps) else - (deps,allhyps)) + (MoveBefore id,deps,allhyps)) hyps - ([x],[]))) in + (MoveBefore x,[x],[]))) in (* In practice, no dep hyps before x, so MoveBefore x is good enough *) (* Decides if x appears in conclusion *) let depconcl = occur_var env x concl in let need_rewrite = not (List.is_empty dephyps) || depconcl in tclTHENLIST ((if need_rewrite then - [revert dephyps; + [revert (List.map snd dephyps); general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp); - (tclMAP intro_using dephyps)] + (tclMAP (fun (dest,id) -> intro_move (Some id) dest) dephyps)] else [Proofview.tclUNIT ()]) @ [tclTRY (clear [x; hyp])]) @@ -1706,17 +1718,6 @@ let default_subst_tactic_flags () = else { only_leibniz = true; rewrite_dependent_proof = false } -let regular_subst_tactic = ref true - -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "more regular behavior of tactic subst"; - optkey = ["Regular";"Subst";"Tactic"]; - optread = (fun () -> !regular_subst_tactic); - optwrite = (:=) regular_subst_tactic } - let subst_all ?(flags=default_subst_tactic_flags ()) () = if !regular_subst_tactic then diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a626092dd..0bb842601 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1836,19 +1836,19 @@ let on_the_bodies = function | [id] -> str " depends on the body of " ++ pr_id id | l -> str " depends on the bodies of " ++ pr_sequence pr_id l -let check_is_type env ty msg = - Proofview.tclEVARMAP >>= fun sigma -> +exception DependsOnBody of Id.t option + +let check_is_type env sigma ty = let evdref = ref sigma in try let _ = Typing.e_sort_of env evdref ty in - Proofview.Unsafe.tclEVARS !evdref + !evdref with e when Errors.noncritical e -> - msg e + raise (DependsOnBody None) -let check_decl env decl msg = +let check_decl env sigma decl = let open Context.Named.Declaration in let ty = get_type decl in - Proofview.tclEVARMAP >>= fun sigma -> let evdref = ref sigma in try let _ = Typing.e_sort_of env evdref ty in @@ -1856,15 +1856,17 @@ let check_decl env decl msg = | LocalAssum _ -> () | LocalDef (_,c,_) -> Typing.e_check env evdref c ty in - Proofview.Unsafe.tclEVARS !evdref + !evdref with e when Errors.noncritical e -> - msg e + let id = get_id decl in + raise (DependsOnBody (Some id)) let clear_body ids = let open Context.Named.Declaration in Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let sigma = Tacmach.New.project gl in let ctx = named_context env in let map = function | LocalAssum (id,t) as decl -> @@ -1878,23 +1880,32 @@ let clear_body ids = let ctx = List.map map ctx in let base_env = reset_context env in let env = push_named_context ctx base_env in - let check_hyps = - let check env decl = - let msg _ = Tacticals.New.tclZEROMSG - (str "Hypothesis " ++ pr_id (get_id decl) ++ on_the_bodies ids) + let check = + try + let check (env, sigma) decl = + (** Do no recheck hypotheses that do not depend *) + let sigma = + if List.exists (fun id -> occur_var_in_decl env id decl) ids then + check_decl env sigma decl + else sigma + in + (push_named decl env, sigma) in - check_decl env decl msg <*> Proofview.tclUNIT (push_named decl env) - in - let checks = Proofview.Monad.List.fold_left check base_env (List.rev ctx) in - Proofview.tclIGNORE checks - in - let check_concl = - let msg _ = Tacticals.New.tclZEROMSG - (str "Conclusion" ++ on_the_bodies ids) - in - check_is_type env concl msg + let (env, sigma) = List.fold_left check (base_env, sigma) (List.rev ctx) in + let sigma = + if List.exists (fun id -> occur_var env id concl) ids then + check_is_type env sigma concl + else sigma + in + Proofview.Unsafe.tclEVARS sigma + with DependsOnBody where -> + let msg = match where with + | None -> str "Conclusion" ++ on_the_bodies ids + | Some id -> str "Hypothesis " ++ pr_id id ++ on_the_bodies ids + in + Tacticals.New.tclZEROMSG msg in - check_hyps <*> check_concl <*> + check <*> Refine.refine ~unsafe:true { run = begin fun sigma -> Evarutil.new_evar env sigma ~principal:true concl end } |