From c6d28beca01809dbd06b3b36ea53bd4a94824083 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 27 Aug 2017 17:07:15 +0200
Subject: Proper handling of rigid variables in subtyping.

---
 tests/rebind.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'tests')

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.
-- 
cgit v1.2.3