diff options
| -rw-r--r-- | doc/changelog/04-tactics/13882-fix-ssr-setoidrw-in-hyp.rst | 6 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 16 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12011.v | 21 |
3 files changed, 35 insertions, 8 deletions
diff --git a/doc/changelog/04-tactics/13882-fix-ssr-setoidrw-in-hyp.rst b/doc/changelog/04-tactics/13882-fix-ssr-setoidrw-in-hyp.rst new file mode 100644 index 0000000000..31b331f0ff --- /dev/null +++ b/doc/changelog/04-tactics/13882-fix-ssr-setoidrw-in-hyp.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Setoid rewriting now remembers the (invisible) binder names of non-dependent product types. SSReflect's rewrite tactic expects these names to be retained when using ``rewrite foo in H``. + This also fixes SSR ``rewrite foo in H *`` erroneously reverting ``H``. + (`#13882 <https://github.com/coq/coq/pull/13882>`_, + fixes `#12011 <https://github.com/coq/coq/issues/12011>`_, + by Gaëtan Gilbert). diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 6d0e0c36b3..c7bda43465 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -251,10 +251,10 @@ end) = struct (** Folding/unfolding of the tactic constants. *) - let unfold_impl sigma t = + let unfold_impl n sigma t = match EConstr.kind sigma t with | App (arrow, [| a; b |])(* when eq_constr arrow (Lazy.force impl) *) -> - mkProd (make_annot Anonymous Sorts.Relevant, a, lift 1 b) + mkProd (make_annot n Sorts.Relevant, a, lift 1 b) | _ -> assert false let unfold_all sigma t = @@ -273,16 +273,16 @@ end) = struct | _ -> assert false) | _ -> assert false - let arrow_morphism env evd ta tb a b = + let arrow_morphism env evd n ta tb a b = let ap = is_Prop (goalevars evd) ta and bp = is_Prop (goalevars evd) tb in - if ap && bp then app_poly env evd impl [| a; b |], unfold_impl + if ap && bp then app_poly env evd impl [| a; b |], unfold_impl n else if ap then (* Domain in Prop, CoDomain in Type *) - (app_poly env evd arrow [| a; b |]), unfold_impl + (app_poly env evd arrow [| a; b |]), unfold_impl n (* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *) else if bp then (* Dummy forall *) - (app_poly env evd coq_all [| a; mkLambda (make_annot Anonymous Sorts.Relevant, a, lift 1 b) |]), unfold_forall + (app_poly env evd coq_all [| a; mkLambda (make_annot n Sorts.Relevant, a, lift 1 b) |]), unfold_forall else (* None in Prop, use arrow *) - (app_poly env evd arrow [| a; b |]), unfold_impl + (app_poly env evd arrow [| a; b |]), unfold_impl n let rec decomp_pointwise sigma n c = if Int.equal n 0 then c @@ -1079,7 +1079,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let arr = if prop then PropGlobal.arrow_morphism else TypeGlobal.arrow_morphism in - let (evars', mor), unfold = arr env evars tx tb x b in + let (evars', mor), unfold = arr env evars n.binder_name tx tb x b in let state, res = aux { state ; env ; unfresh ; term1 = mor ; ty1 = ty ; cstr = (prop,cstr) ; evars = evars' } in diff --git a/test-suite/bugs/closed/bug_12011.v b/test-suite/bugs/closed/bug_12011.v new file mode 100644 index 0000000000..f149b4e8ae --- /dev/null +++ b/test-suite/bugs/closed/bug_12011.v @@ -0,0 +1,21 @@ +From Coq Require Import Setoid ssreflect. + +Lemma test A (R : relation A) `{Equivalence _ R} (x y z : A) : + R x y -> R y z -> R x z. +Proof. + intros Hxy Hyz. + rewrite -Hxy in Hyz. + exact Hyz. +Qed. + + + +Axiom envs_lookup_delete : bool. +Axiom envs_lookup_delete_Some : envs_lookup_delete = true <-> False. + +Goal envs_lookup_delete = true -> False. +Proof. +intros Hlookup. +rewrite envs_lookup_delete_Some in Hlookup *. (* <- used to revert Hlookup *) +exact Hlookup. +Qed. |