From eb067dc862c5a7acea2b92cabe867bfc9dcdaf92 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 11 Jun 2010 10:16:44 +0000
Subject: Mainly made that evarconv is able to solve "?n = (fun x => x) ?n"
 (sic). Use two ways to solve it: - added a whd_betaiota in solve_simple_eqn
 (since evarconv itself   refuses beta to preserve the opportunities of
 first-order-matching   expressions of the form "(fun x => P) t"; an advantage
 of this   whd_betaiota is also that it may simplify K-redexes. - also added a
 last-chance test in case of failing occur-check by   trying to fully
 head-normalize (with delta) the right-hand-side   (allows to solve for
 instance "?n = id ?n" where id is a constant   (a bridled form of solve_refl
 that use fconv instead of evar_conv_x). Incidentally improved a bit the
 rendering of the type of generalized terms in pattern-matching by using
 whd_betaiota.

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

(limited to 'test-suite')

diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index a8cc7f745a..4aa00e689f 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -52,3 +52,18 @@ Hint Resolve -> a.
 Goal forall n, n=0 -> n<=0.
 auto.
 Qed.
+
+
+(* This example comes from Chlipala's ltamer *)
+(* It used to fail from r12902 to r13112 since type_of started to call *)
+(* e_cumul (instead of conv_leq) which was not able to unify "?id" and *)
+(* "(fun x => x) ?id" *)
+
+Notation "e :? pf" := (eq_rect _ (fun X : Set => X) e _ pf)
+  (no associativity, at level 90).
+
+Axiom cast_coalesce :
+  forall (T1 T2 T3 : Set) (e : T1) (pf1 : T1 = T2) (pf2 : T2 = T3),
+  ((e :? pf1) :? pf2) = (e :? trans_eq pf1 pf2).
+
+Hint Rewrite cast_coalesce : ltamer.
-- 
cgit v1.2.3