diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-07 15:24:16 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-24 18:03:56 +0100 |
| commit | e59d58b6db222332f7d7ad2adcb2b78c24fb351e (patch) | |
| tree | f96740aedb3b99c54afd233e087a29b20a59cae3 /test-suite/output/ltac.out | |
| parent | c1e670b386f83ed78104a6eb6e4d17cc1d906439 (diff) | |
Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).
Was broken since 8.6.
Diffstat (limited to 'test-suite/output/ltac.out')
| -rw-r--r-- | test-suite/output/ltac.out | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index c5d58ec1e..7f3cdad6c 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -32,7 +32,7 @@ nat 0 0 Ltac foo := - let x := intros ** in + let x := intros in let y := intros -> in let v := constr:(nil) in let w := () in |