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.

---
 src/tac2intern.ml |  8 ++------
 tests/rebind.v    | 10 ++++++++++
 2 files changed, 12 insertions(+), 6 deletions(-)

diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index ef0763ff8e..40e0ffb34e 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -1167,12 +1167,8 @@ let intern_open_type t =
 let check_subtype t1 t2 =
   let env = empty_env () in
   let t1 = fresh_type_scheme env t1 in
-  (** We build a substitution mimicking rigid variable by using dummy refs *)
-  let mb = MBId.make DirPath.empty (Id.of_string "_t") in
-  let rigid i =
-    let kn = KerName.make (MPbound mb) DirPath.empty (Label.make "_t") in
-    GTypRef (Other kn, [])
-  in
+  (** We build a substitution mimicking rigid variable by using dummy tuples *)
+  let rigid i = GTypRef (Tuple i, []) in
   let (n, t2) = t2 in
   let subst = Array.init n rigid in
   let substf i = subst.(i) in
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