summaryrefslogtreecommitdiff
path: root/test-suite/output/ltac_missing_args.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output/ltac_missing_args.v')
-rw-r--r--test-suite/output/ltac_missing_args.v19
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v
new file mode 100644
index 00000000..91331a1d
--- /dev/null
+++ b/test-suite/output/ltac_missing_args.v
@@ -0,0 +1,19 @@
+Ltac foo x := idtac x.
+Ltac bar x := fun y _ => idtac x y.
+Ltac baz := foo.
+Ltac qux := bar.
+Ltac mydo tac := tac ().
+Ltac rec x := rec.
+
+Goal True.
+ Fail foo.
+ Fail bar.
+ Fail bar True.
+ Fail baz.
+ Fail qux.
+ Fail mydo ltac:(fun _ _ => idtac).
+ Fail let tac := (fun _ => idtac) in tac.
+ Fail (fun _ => idtac).
+ Fail rec True.
+ Fail let rec tac x := tac in tac True.
+Abort.