Add a regression test for "Allow catching of WrongAbstractionType, fixing a regression from 8.4 … git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16389 85f007b7-540e-0410-9357-904b9bb8a0f7"

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#3022
From: @JasonGross
Reported version: 8.5
CC: @JasonGross, @ppedrot

[coqbot]

Comment author: @JasonGross

The most recent commit on trunk was the result of my bug report at HoTT#28.

The following code serves as a regression test for this bug (at least for now), if you want to include it as a test case

Goal forall (O obj : Type) (f : O -> obj) (x : O) (e : x = x)
(T : obj -> obj -> Type) (m : forall x0 : obj, T x0 x0),
match eq_sym e in (_ = y) return (T (f y) (f x)) with
| eq_refl => m (f x)
end = m (f x).
intros.
try case e.