diff options
| author | Pierre-Marie Pédrot | 2021-03-08 18:22:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-10 12:23:41 +0100 |
| commit | 83c11db006ca87b3912d2548593b669884a3b4b5 (patch) | |
| tree | df57a5c88262fb5ff0d4d5a27749adb3b24cc40e | |
| parent | 234a802f0925f9c9078417afa28dcb00c31668d9 (diff) | |
Adding output tests.
| -rw-r--r-- | test-suite/output/ltac2_deprecated.out | 12 | ||||
| -rw-r--r-- | test-suite/output/ltac2_deprecated.v | 15 |
2 files changed, 27 insertions, 0 deletions
diff --git a/test-suite/output/ltac2_deprecated.out b/test-suite/output/ltac2_deprecated.out new file mode 100644 index 0000000000..d17b719bcd --- /dev/null +++ b/test-suite/output/ltac2_deprecated.out @@ -0,0 +1,12 @@ +File "stdin", line 13, characters 11-14: +Warning: Ltac2 definition foo is deprecated. test_definition +[deprecated-ltac2-definition,deprecated] +- : unit = () +File "stdin", line 14, characters 11-14: +Warning: Ltac2 alias bar is deprecated. test_notation +[deprecated-ltac2-alias,deprecated] +- : unit = () +File "stdin", line 15, characters 11-14: +Warning: Ltac2 definition qux is deprecated. test_external +[deprecated-ltac2-definition,deprecated] +- : 'a array -> int = <fun> diff --git a/test-suite/output/ltac2_deprecated.v b/test-suite/output/ltac2_deprecated.v new file mode 100644 index 0000000000..9598a5979c --- /dev/null +++ b/test-suite/output/ltac2_deprecated.v @@ -0,0 +1,15 @@ +Require Import Ltac2.Ltac2. + +#[deprecated(note="test_definition")] +Ltac2 foo := (). + +#[deprecated(note="test_notation")] +Ltac2 Notation bar := (). + +#[deprecated(note="test_external")] +Ltac2 @ external qux : 'a array -> int := "ltac2" "array_length". +(* Randomly picked external function *) + +Ltac2 Eval foo. +Ltac2 Eval bar. +Ltac2 Eval qux. |