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

1 files changed, 23 insertions, 0 deletions

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.