diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-09 17:09:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-09 17:09:59 +0200 |
| commit | a9efa6f9e601cc2bfa1968dca1cdc0d01ebf55e8 (patch) | |
| tree | d0c52f66d7c5c85f13c585ac4de19ea33550bd6f /test-suite/output/Errors.out | |
| parent | ff980722521812d19bc1e25cd504567b4a6b549a (diff) | |
Fix output test-suite after commit 0d3c319.
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 62e9ef4b2..06a6b2d15 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -6,5 +6,5 @@ The command has indeed failed with message: In nested Ltac calls to "f" and "apply x", last call failed. Unable to unify "nat" with "True". The command has indeed failed with message: -Ltac call to "instantiate" failed. +Ltac call to "instantiate ( (ident) := (lglob) )" failed. Error: Instance is not well-typed in the environment of ?x. |