diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-05 22:47:39 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-05 22:47:39 +0000 |
| commit | 742ef62fe8050a6865d06bd644e30cbec0e7eb02 (patch) | |
| tree | 7b8db9bbebcb92e59a68bbb7508184dc574dc643 /test-suite | |
| parent | df313cefbaddb57f89650171e59e3abcb168a273 (diff) | |
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
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Case19.v | 11 |
1 files changed, 11 insertions, 0 deletions
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). |