diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-08 15:31:56 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-08 15:35:59 +0200 |
| commit | 0cebd2b86a90cc1361bcfac6bb097540e22c9a21 (patch) | |
| tree | 648ece59fd72185da10d71771d9f858aa1fa7fd4 /test-suite/output/Errors.out | |
| parent | 6a3767e48e91604071b5709a6658aa2f255a4522 (diff) | |
Fixing output test-suite: since universe polymorphism, the Print command
shows the polymorphism status of the term.
Diffstat (limited to 'test-suite/output/Errors.out')
| -rw-r--r-- | test-suite/output/Errors.out | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index 839611b65..bcc37b635 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -4,4 +4,4 @@ The command has indeed failed with message: => Error: Unable to unify "nat" with "True". The command has indeed failed with message: => In nested Ltac calls to "f" and "apply x", last call failed. - Error: Unable to unify "nat" with "True". +Error: Unable to unify "nat" with "True". |