From 90069c14ff393c33efdf7477bda096f5ba684bc1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Mar 2008 08:22:58 +0000
Subject: Correction d'un bug "ancestral": apply ne savait pas unifier ?n=?n
 dans certains cas. Branchement au passage de w_unify vers evar_conv et
 solve_simple_eqn en cas d'équations entre Evars.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10623 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/unification.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 6a4d928512..e31d67d8cd 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -96,3 +96,16 @@ Goal (forall x, 0 * x = 0 -> True) -> True.
 intros; eapply H.
 rewrite <- plus_n_Sm. (* should refine ?x with S ?x' *)
 Abort.
+
+(* Check handling of identity equation between evars *)
+(* The example failed to pass until revision 10623 *)
+
+Lemma l6 :
+  (forall y, (forall x, (forall z, y = 0 -> y + z = 0) -> y + x = 0) -> True)
+  -> True.
+intros.
+eapply H.
+intros.
+apply H0. (* Check that equation ?n[H] = ?n[H] is correctly considered true *)
+reflexivity.
+Qed.
-- 
cgit v1.2.3