diff options
| author | Pierre-Marie Pédrot | 2017-08-27 17:07:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-27 17:15:55 +0200 |
| commit | c6d28beca01809dbd06b3b36ea53bd4a94824083 (patch) | |
| tree | d9cd7edcf1299cfd222550b2a018a7b6763c1f66 /tests | |
| parent | 9bbdee3c09c92654bb8937b9939a9b9c69c23d1d (diff) | |
Proper handling of rigid variables in subtyping.
Diffstat (limited to 'tests')
| -rw-r--r-- | tests/rebind.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/tests/rebind.v b/tests/rebind.v index 270fdd0b69..e1c20a2059 100644 --- a/tests/rebind.v +++ b/tests/rebind.v @@ -22,3 +22,13 @@ Ltac2 bar () := (). (** Cannot redefine non-mutable tactics *) Fail Ltac2 Set bar := fun _ => (). + +(** Subtype check *) + +Ltac2 mutable rec f x := f x. + +Fail Ltac2 Set f := fun x => x. + +Ltac2 mutable g x := x. + +Ltac2 Set g := f. |