diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-17 14:56:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-17 14:56:04 +0000 |
| commit | 8ac929ea128f1f7353b3f4d532b642e769542e55 (patch) | |
| tree | b77b28d76ae301b4af81e18309bff869625c6f99 /test-suite/output/names.out | |
| parent | 97fc36f552bfd9731ac47716faf2b02d4555eb07 (diff) | |
Added propagation of evars unification failure reasons for better
error messages. The architecture of unification error handling
changed, not helped by ocaml for checking that every exceptions is
correctly caught. Report or fix if you find a regression.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16205 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/names.out')
| -rw-r--r-- | test-suite/output/names.out | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/names.out b/test-suite/output/names.out index 90ad4ba09..1f13619cb 100644 --- a/test-suite/output/names.out +++ b/test-suite/output/names.out @@ -2,4 +2,4 @@ The command has indeed failed with message: => Error: In environment y : nat The term "a y" has type "{y0 : nat | y = y0}" - while it is expected to have type "{x : nat | x = y}". + while it is expected to have type "{x : nat | x = y}". |