From 742ef62fe8050a6865d06bd644e30cbec0e7eb02 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 5 May 2013 22:47:39 +0000 Subject: Hack to solve a "Bad recursive type" anomaly. Retyping expects its argument already well-typed. However, if unification problems are not fully solved, a term to match can have an evar type together with the constraint that this evar has to be convertible to some given inductive type. One could have tried to have a more eager resolution of unification constraint but I'm afraid of the cost in comparing c=c' in general in "?x[c] = c'" unification problems, so I instead added a hack in retyping to recover the constraint. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16471 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/success/Case19.v | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'test-suite') diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v index 9a6ed71a5..c29e52978 100644 --- a/test-suite/success/Case19.v +++ b/test-suite/success/Case19.v @@ -6,3 +6,14 @@ Variable T : Type. Variable x : nat*nat. Check let (_, _) := x in sigT (fun _ : T => nat). + +(* This used to raise an anomaly in V8.4, up to pl2 *) + +Goal {x: nat & x=x}. +Fail exists (fun x => + match + projT2 (projT2 x) as e in (_ = y) + return _ = existT _ (projT1 x) (existT _ y e) + with + | eq_refl => eq_refl + end). -- cgit v1.2.3