diff options
| -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 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. diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 21554e9ff..f4254e4e2 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. |