aboutsummaryrefslogtreecommitdiff
path: root/tests/stuff
diff options
context:
space:
mode:
Diffstat (limited to 'tests/stuff')
-rw-r--r--tests/stuff/ltac2.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/tests/stuff/ltac2.v b/tests/stuff/ltac2.v
index 86ab5afb17..4950a20ec4 100644
--- a/tests/stuff/ltac2.v
+++ b/tests/stuff/ltac2.v
@@ -120,6 +120,7 @@ Abort.
Goal True.
Proof.
+
let x () := plus (fun () => 0) (fun _ => 1) in
match case x with
| Val x =>