diff options
| author | Pierre-Marie Pédrot | 2016-09-09 17:09:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-09 17:09:59 +0200 |
| commit | a9efa6f9e601cc2bfa1968dca1cdc0d01ebf55e8 (patch) | |
| tree | d0c52f66d7c5c85f13c585ac4de19ea33550bd6f | |
| parent | ff980722521812d19bc1e25cd504567b4a6b549a (diff) | |
Fix output test-suite after commit 0d3c319.
| -rw-r--r-- | test-suite/output/Errors.out | 2 | ||||
| -rw-r--r-- | test-suite/output/ltac.out | 17 |
2 files changed, 12 insertions, 7 deletions
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index 62e9ef4b20..06a6b2d157 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. diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 21554e9ff8..f4254e4e2f 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -4,20 +4,25 @@ Ltac f x y z := symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize dependent z The command has indeed failed with message: -In nested Ltac calls to "g1" and "refine", last call failed. +In nested Ltac calls to "g1" and "refine (uconstr)", last call failed. The term "I" has type "True" while it is expected to have type "False". The command has indeed failed with message: -In nested Ltac calls to "f1" and "refine", last call failed. +In nested Ltac calls to "f1 (constr)" and "refine (uconstr)", last call +failed. The term "I" has type "True" while it is expected to have type "False". The command has indeed failed with message: -In nested Ltac calls to "g2", "g1" and "refine", last call failed. +In nested Ltac calls to "g2 (constr)", "g1" and "refine (uconstr)", last call +failed. The term "I" has type "True" while it is expected to have type "False". The command has indeed failed with message: -In nested Ltac calls to "f2", "f1" and "refine", last call failed. +In nested Ltac calls to "f2", "f1 (constr)" and "refine (uconstr)", last call +failed. The term "I" has type "True" while it is expected to have type "False". The command has indeed failed with message: -In nested Ltac calls to "h" and "injection", last call failed. +In nested Ltac calls to "h" and "injection (destruction_arg)", last call +failed. Error: No primitive equality found. The command has indeed failed with message: -In nested Ltac calls to "h" and "injection", last call failed. +In nested Ltac calls to "h" and "injection (destruction_arg)", last call +failed. Error: No primitive equality found. |