Merge branch 'fix-unnamed-default-name' into 'master'

Set default name for unnamed binders to H

Closes #337

See merge request iris/iris!484

tests/proofmode.ref

@@ -94,6 +94,19 @@ Tactic failure: iExistDestruct: cannot destruct P.
   --------------------------------------□
   P
   
+"test_iDestruct_exists_anonymous"
+     : string
+1 subgoal
+  
+  PROP : bi
+  P : PROP
+  Φ : nat → PROP
+  H : nat
+  ============================
+  "HΦ" : ∃ x : nat, Φ x
+  --------------------------------------∗
+  ∃ x : nat, Φ x
+  
 "test_iIntros_forall_pure"
      : string
 1 subgoal

tests/proofmode.v

@@ -184,6 +184,18 @@ Proof.
   iExists y0; auto.
 Qed.
 
+(* regression test for #337 *)
+Check "test_iDestruct_exists_anonymous".
+Lemma test_iDestruct_exists_anonymous P Φ :
+  (∃ _:nat, P) ∗ (∃ x:nat, Φ x) -∗ P ∗ ∃ x, Φ x.
+Proof.
+  iIntros "[HP HΦ]".
+  (* this should not use [x] as the default name for the unnamed binder *)
+  iDestruct "HP" as (?) "$". Show.
+  iDestruct "HΦ" as (x) "HΦ".
+  by iExists x.
+Qed.
+
 Definition an_exists P : PROP := (∃ (an_exists_name:nat), ▷^an_exists_name P)%I.
 
 (* should use the name from within [an_exists] *)

theories/proofmode/ident_name.v

@@ -27,8 +27,11 @@ Arguments as_ident_name {A B f} name : assert.
 
 Ltac solve_as_ident_name :=
   lazymatch goal with
-  | |- AsIdentName (λ x, _) _ =>
-    let name := to_ident_name x in
+  (* The [H] here becomes the default name if the binder is anonymous. We use
+     [H] with the idea that an unnamed and unused binder is likely to be a
+     proposition. *)
+  | |- AsIdentName (λ H, _) _ =>
+    let name := to_ident_name H in
     notypeclasses refine (as_ident_name name)
   | _ => notypeclasses refine (to_ident_name __unknown)
   end.