From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- test-suite/output/ltac_missing_args.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 test-suite/output/ltac_missing_args.v (limited to 'test-suite/output/ltac_missing_args.v') 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. -- cgit v1.2.3