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.