diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-11 15:05:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-11 15:21:33 +0200 |
| commit | ae5305a4837cce3c7fd61b92ce8110ac66ec2750 (patch) | |
| tree | 3026a62e18044a3126521c0c72eefe8304184262 /test-suite/output/ltac.out | |
| parent | 2e07ecfce221840047b2f95c93acdb79a4fe0985 (diff) | |
Refining 0c320e79ba30 in fixing interpretation of constr under binders
which was broken after it became possible to have binding names
themselves bound to ltac variables (2fcc458af16b).
Interpretation was corrected, but error message was damaged.
Diffstat (limited to 'test-suite/output/ltac.out')
| -rw-r--r-- | test-suite/output/ltac.out | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out new file mode 100644 index 000000000..d003c70df --- /dev/null +++ b/test-suite/output/ltac.out @@ -0,0 +1,2 @@ +The command has indeed failed with message: +Error: Ltac variable y depends on pattern variable name z which is not bound in current context. |