From bffa084eec75371c7df991c7a88aca5fe65114da Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 10 Nov 2020 16:52:51 +0100
Subject: Finish fixing setoid rewrite under anonymous lambdas (hopefully)

Fix #13246

Not sure if this is the right thing to do, but it seems to work.
---
 plugins/ltac/rewrite.ml            | 12 +++++--
 test-suite/bugs/closed/bug_13246.v | 69 ++++++++++++++++++++++++++++++++++++++
 2 files changed, 78 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_13246.v

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 26e2b18a02..76a2b6fade 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
diff --git a/test-suite/bugs/closed/bug_13246.v b/test-suite/bugs/closed/bug_13246.v
new file mode 100644
index 0000000000..11f5baaaf4
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13246.v
@@ -0,0 +1,69 @@
+Axiom _0: Prop.
+
+From Coq Require Export Morphisms Setoid Utf8.
+
+Class Equiv A := equiv: relation A.
+
+Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
+Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
+Reserved Notation "■ P" (at level 20, right associativity).
+
+(** Define the scope *)
+Declare Scope bi_scope.
+Delimit Scope bi_scope with I.
+
+Structure bi :=
+  Bi { bi_car :> Type;
+       bi_entails : bi_car → bi_car → Prop;
+       bi_impl : bi_car → bi_car → bi_car;
+       bi_forall : ∀ A, (A → bi_car) → bi_car; }.
+
+Declare Instance bi_equiv `{PROP:bi} : Equiv (bi_car PROP).
+
+Arguments bi_car : simpl never.
+Arguments bi_entails {PROP} _%I _%I : simpl never, rename.
+Arguments bi_impl {PROP} _%I _%I : simpl never, rename.
+Arguments bi_forall {PROP _} _%I : simpl never, rename.
+
+Notation "P ⊢ Q" := (bi_entails P%I Q%I) .
+Notation "P ⊣⊢ Q" := (equiv (A:=bi_car _) P%I Q%I) .
+
+Infix "→" := bi_impl : bi_scope.
+Notation "∀ x .. y , P" :=
+  (bi_forall (λ x, .. (bi_forall (λ y, P)) ..)%I) : bi_scope.
+
+(* bug disappears if definitional class *)
+Class Plainly (PROP : bi) := { plainly : PROP -> PROP; }.
+Notation "■ P" := (plainly P) : bi_scope.
+
+Section S.
+  Context {I : Type} {PROP : bi} `(Plainly PROP).
+
+  Lemma plainly_forall `{Plainly PROP} {A} (Ψ : A → PROP) : (∀ a, ■ (Ψ a)) ⊣⊢ ■ (∀ a, Ψ a).
+  Proof. Admitted.
+
+  Global Instance entails_proper :
+    Proper (equiv ==> equiv ==> iff) (bi_entails : relation PROP).
+  Proof. Admitted.
+
+  Global Instance impl_proper :
+    Proper (equiv ==> equiv ==> equiv) (@bi_impl PROP).
+  Proof. Admitted.
+
+  Global Instance forall_proper A :
+    Proper (pointwise_relation _ equiv ==> equiv) (@bi_forall PROP A).
+  Proof. Admitted.
+
+  Declare Instance PROP_Equivalence: Equivalence (@equiv PROP _).
+
+  Set Mangle Names.
+  Lemma foo (P : I -> PROP) K:
+    K ⊢ ∀ (j : I)
+          (_ : Prop) (* bug disappears if this is removed *)
+      , (∀ i0, ■ P i0) → P j.
+  Proof.
+    setoid_rewrite plainly_forall.
+    (* retype in case the tactic did some nonsense *)
+    match goal with |- ?T => let _ := type of T in idtac end.
+  Abort.
+End S.
-- 
cgit v1.2.3