diff options
| author | herbelin | 2011-10-05 14:34:17 +0000 |
|---|---|---|
| committer | herbelin | 2011-10-05 14:34:17 +0000 |
| commit | b7fcbb07f8b484707a86eb06df1bd7116fb55a21 (patch) | |
| tree | bf2bc42cc3cf39131f98f8fe687b3079bbba45d2 /test-suite | |
| parent | d566330747374ba13d6b52424d53ab7d84cc921e (diff) | |
It happens that the type inference algorithm (pretyping) did not check
that the return predicate of the match construction is at an allowed
sort, resulting in tactics possibly manipulating ill-typed terms. This
is now fixed,
Incidentally removed in pretyping an ill-placed coercion.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14508 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/change.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/success/change.v b/test-suite/success/change.v index 5ac6ce82b5..c65cf3036c 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -30,3 +30,11 @@ change 3 at 1 with (1+2) in H |- *. change 3 at 1 with (1+2) in H, H|-. change 3 in |- * at 1. *) + +(* Test that pretyping checks allowed elimination sorts *) + +Goal True. +Fail change True with (let (x,a) := ex_intro _ True (eq_refl True) in x). +Fail change True with + match ex_intro _ True (eq_refl True) with ex_intro x _ => x end. +Abort. |