aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/tac2intern.ml8
1 files changed, 2 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