diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-11 09:02:16 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-11 09:02:16 +0000 |
| commit | 4564079be1b9e3ecdbe988e726d8e77d3059d02e (patch) | |
| tree | 19465587be14516e24eddd3b6bafb2c3d1dda231 /test-suite/failure | |
| parent | 2cbf0f8fe0929d36391a8f12e32873eb3a95d7cd (diff) | |
Relatively ad hoc fix to an ill-typed instantiation bug in type
inference (see file failure/evar1.v) + fix of some CUMUL problems that
were in the wrong direction. We assume for the fix that ill-typed
unification problems come from subtyping where we don't know yet if a
coercion has to be inserted or not, and hence are of the CUMUL
form. More on suspending problems of the form ?n <= Type or Prop <= ?n
has to be done yet.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12268 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/failure')
| -rw-r--r-- | test-suite/failure/evar1.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/test-suite/failure/evar1.v b/test-suite/failure/evar1.v new file mode 100644 index 000000000..1a4e42a89 --- /dev/null +++ b/test-suite/failure/evar1.v @@ -0,0 +1,3 @@ +(* This used to succeed by producing an ill-typed term in v8.2 *) + +Lemma u: forall A : Prop, (exist _ A A) = (exist _ A A). |