diff options
Diffstat (limited to 'test-suite/output/ltac.out')
| -rw-r--r-- | test-suite/output/ltac.out | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index eb9f571022..efdc94fb1e 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -38,3 +38,14 @@ Ltac foo := let w := () in let z := 1 in pose v +2 subgoals + + n : nat + ============================ + (fix a (n0 : nat) : nat := match n0 with + | 0 => 0 + | S n1 => a n1 + end) n = n + +subgoal 2 is: + forall a : nat, a = 0 |