diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-07-09 22:16:10 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-07-09 22:16:10 +0200 |
commit | a4909dd5f8d5df773a361a7cbacefc392b7cfebd (patch) | |
tree | 7f16c4018bad54d9c1bf7c9e9d4aefacd83b2e40 /test-suite | |
parent | c1d4dc68ace54f9ff9fd8f6466add38098ef0495 (diff) | |
parent | 420b38cba7aedfcfeac5671a7db0c02c4bb14a0c (diff) |
Merge PR #7920: Generic syntax for attributes
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/success/attribute-syntax.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v new file mode 100644 index 000000000..83fb3d0c8 --- /dev/null +++ b/test-suite/success/attribute-syntax.v @@ -0,0 +1,23 @@ +From Coq Require Program. + +Section Scope. + +#[local] Coercion nat_of_bool (b: bool) : nat := + if b then 0 else 1. + +Check (refl_equal : true = 0 :> nat). + +End Scope. + +Fail Check 0 = true :> nat. + +#[polymorphic] +Definition ι T (x: T) := x. + +Check ι _ ι. + +#[program] +Fixpoint f (n: nat) {wf lt n} : nat := _. + +#[deprecated(since="8.9.0")] +Ltac foo := foo. |