diff options
| author | Michael Soegtrop | 2021-03-23 21:55:59 +0100 |
|---|---|---|
| committer | Michael Soegtrop | 2021-03-23 21:55:59 +0100 |
| commit | 47c20236f578dca9381822a62b5a406d6b42676d (patch) | |
| tree | fef686014dc1985799869ff1d6cab4e8f76ec8bc /test-suite | |
| parent | fa2ba1571cbd791c3b1acd87adeacd0aa4bd6e88 (diff) | |
| parent | 83c11db006ca87b3912d2548593b669884a3b4b5 (diff) | |
Merge PR #13774: Allow to register deprecation status in Ltac2 term and notation declarations
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle
Diffstat (limited to 'test-suite')
| -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. |