diff options
Diffstat (limited to 'test-suite/output/ltac.out')
| -rw-r--r-- | test-suite/output/ltac.out | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 35c3057d84..c5d58ec1ec 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -31,3 +31,10 @@ nat nat 0 0 +Ltac foo := + let x := intros ** in + let y := intros -> in + let v := constr:(nil) in + let w := () in + let z := 1 in + pose v |