diff options
| -rw-r--r-- | tactics/equality.ml | 61 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4214.v | 5 | ||||
| -rw-r--r-- | theories/Lists/List.v | 2 |
3 files changed, 47 insertions, 21 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 5d6fcc5b1..f2860a230 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1589,10 +1589,10 @@ let is_eq_x gl x (id,_,c) = erase hyp and x; proceed by generalizing all dep hyps *) let subst_one dep_proof_ok x (hyp,rhs,dir) = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let hyps = Proofview.Goal.hyps gl in - let concl = Proofview.Goal.concl gl in + let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + 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 (id,b,_ as dcl) (deps,allhyps) -> @@ -1663,24 +1663,45 @@ let default_subst_tactic_flags () = { only_leibniz = true; rewrite_dependent_proof = false } let subst_all ?(flags=default_subst_tactic_flags ()) () = - Proofview.Goal.nf_enter begin fun gl -> - let find_eq_data_decompose = find_eq_data_decompose gl in - let test (_,c) = - try - let lbeq,u,(_,x,y) = find_eq_data_decompose c in - let eq = Universes.constr_of_global_univ (lbeq.eq,u) in - if flags.only_leibniz then restrict_to_eq_and_identity eq; - (* J.F.: added to prevent failure on goal containing x=x as an hyp *) - if Term.eq_constr x y then failwith "caught"; - match kind_of_term x with Var x -> x | _ -> - match kind_of_term y with Var y -> y | _ -> failwith "caught" - with Constr_matching.PatternMatchingFailure -> failwith "caught" + + (* First step: find hypotheses to treat in linear time *) + let find_equations gl = + let gl = Proofview.Goal.assume gl in + let find_eq_data_decompose = find_eq_data_decompose gl in + let test (hyp,_,c) = + try + let lbeq,u,(_,x,y) = find_eq_data_decompose c in + let eq = Universes.constr_of_global_univ (lbeq.eq,u) in + if flags.only_leibniz then restrict_to_eq_and_identity eq; + (* J.F.: added to prevent failure on goal containing x=x as an hyp *) + if Term.eq_constr x y then None else + match kind_of_term x, kind_of_term y with + | Var _, _ | _, Var _ -> Some hyp + | _ -> None + with Constr_matching.PatternMatchingFailure -> None + in + let hyps = Proofview.Goal.hyps gl in + List.map_filter test hyps + in + + (* Second step: treat equations *) + let process hyp = + Proofview.Goal.enter begin fun gl -> + let gl = Proofview.Goal.assume gl in + let find_eq_data_decompose = find_eq_data_decompose gl in + let (_,_,c) = pf_get_hyp hyp gl in + let _,_,(_,x,y) = find_eq_data_decompose c in + (* J.F.: added to prevent failure on goal containing x=x as an hyp *) + if Term.eq_constr x y then Proofview.tclUNIT () else + match kind_of_term x, kind_of_term y with + | Var x, _ -> subst_one flags.rewrite_dependent_proof x (hyp,y,true) + | _, Var y -> subst_one flags.rewrite_dependent_proof y (hyp,x,false) + | _ -> Proofview.tclUNIT () + end in - let test p = try Some (test p) with Failure _ -> None in - let hyps = pf_hyps_types gl in - let ids = List.map_filter test hyps in - let ids = List.uniquize ids in - subst_gen flags.rewrite_dependent_proof ids + Proofview.Goal.nf_enter begin fun gl -> + let ids = find_equations gl in + tclMAP process ids end (* Rewrite the first assumption for which a condition holds diff --git a/test-suite/bugs/closed/4214.v b/test-suite/bugs/closed/4214.v new file mode 100644 index 000000000..cd53c898e --- /dev/null +++ b/test-suite/bugs/closed/4214.v @@ -0,0 +1,5 @@ +(* Check that subst uses all equations around *) +Goal forall A (a b c : A), b = a -> b = c -> a = c. +intros. +subst. +reflexivity. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index ea07a8497..5819fbe5e 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -2202,7 +2202,7 @@ Section ForallPairs. Proof. induction 1. inversion 1. - simpl; destruct 1; destruct 1; repeat subst; auto. + simpl; destruct 1; destruct 1; subst; auto. right; left. apply -> Forall_forall; eauto. right; right. apply -> Forall_forall; eauto. Qed. |