diff options
| -rw-r--r-- | src/tac2intern.ml | 8 | ||||
| -rw-r--r-- | 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. |