Merge PR #7257: Fixing yet a source of dependency on alphabetic order in unification.

3 files changed, 39 insertions, 6 deletions

diff --git a/test-suite/bugs/closed/2670.v b/test-suite/bugs/closed/2670.v
index c401420e94..791889b24b 100644
--- a/test-suite/bugs/closed/2670.v
+++ b/test-suite/bugs/closed/2670.v
@@ -15,6 +15,14 @@ Proof.
   refine (match e return _ with refl_equal => _ end).
   reflexivity.
   Undo 2.
+  (** Check insensitivity to alphabetic order *)
+  refine (match e as a in _ = b return _ with refl_equal => _ end).
+  reflexivity.
+  Undo 2.
+  (** Check insensitivity to alphabetic order *)
+  refine (match e as z in _ = y return _ with refl_equal => _ end).
+  reflexivity.
+  Undo 2.
   (* Next line similarly has a dependent and a non dependent solution *)
   refine (match e with refl_equal => _ end).
   reflexivity.
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index b60b1ee863..94b86fc222 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -125,13 +125,15 @@ s
      : nat
 fun _ : nat => 9
      : nat -> nat
-fun (x : nat) (p : x = x) => match p with
-                             | ONE => ONE
-                             end = p
+fun (x : nat) (p : x = x) =>
+match p in (_ = n) return (n = n) with
+| ONE => ONE
+end = p
      : forall x : nat, x = x -> Prop
-fun (x : nat) (p : x = x) => match p with
-                             | 1 => 1
-                             end = p
+fun (x : nat) (p : x = x) =>
+match p in (_ = n) return (n = n) with
+| 1 => 1
+end = p
      : forall x : nat, x = x -> Prop
 bar  0
      : nat
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index b287b5facf..e1df9ba84a 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -559,3 +559,26 @@ split.
 - (* clear b:True *) match goal with H:_ |- _ => clear H end.
   (* use a:0=0 *) match goal with H:_ |- _ => exact H end.
 Qed.
+
+(* Test choice of most dependent solution *)
+Goal forall n, n = 0 -> exists p, p = n /\ p = 0.
+intros. eexists ?[p]. split. rewrite H.
+reflexivity. (* Compatibility tells [?p:=n] rather than [?p:=0] *)
+exact H. (* this checks that the goal is [n=0], not [0=0] *)
+Qed.
+
+(* Check insensitivity to alphabetic order of names*)
+(* In both cases, the last name is conventionally chosen *)
+(* Before 8.9, the name coming first in alphabetic order *)
+(* was chosen. *)
+Goal forall m n, m = n -> n = 0 -> exists p, p = n /\ p = 0.
+intros. eexists ?[p]. split. rewrite H.
+reflexivity.
+exact H0.
+Qed.
+
+Goal forall n m, n = m -> m = 0 -> exists p, p = m /\ p = 0.
+intros. eexists ?[p]. split. rewrite H.
+reflexivity.
+exact H0.
+Qed.