Library Mtac2Tests.bug_universes

From Mtac2 Require Import Mtac2.

Set Printing Universes.

Definition test@{i j} : Type@{i} -> Type@{max(i,j)} := id.

Lemma testL@{i j} : Type@{i} -> Type@{max(i,j)}.
Proof. exact id. Qed.

Lemma testM@{i j} : Type@{i} -> Type@{max(i,j)}.
MProof.
M.ret id.
Qed.

Lemma testMTac@{i j} : Type@{i} -> Type@{max(i,j)}.
MProof.
T.exact id.
Qed.

Lemma testMTacApply@{i j} : Type@{i} -> Type@{max(i,j)}.
MProof.
T.apply (@id).
Fail Qed.
Abort.

Lemma testLApply@{i j} : Type@{i} -> Type@{max(i,j)}.
Proof. apply @id. Qed.

Notation "p '=e>' b" := (pbase p%core (fun _ => b%core) UniEvarconv)
  (no associativity, at level 201) : pattern_scope.
Notation "p '=e>' [ H ] b" := (pbase p%core (fun H => b%core) UniEvarconv)
  (no associativity, at level 201, H at next level) : pattern_scope.

Definition test_match {A:Type} (x:A) : tactic :=
  mmatch A with
  | [? B] B =e> T.exact x
  end.

Lemma testMmatch@{i j} : Type@{i} -> Type@{max(i,j)}.
MProof.
test_match (fun x=>x).
Qed.

Lemma testMmatch' : Type -> Type.
MProof.
test_match (fun x=>x).
Qed.
Print testMmatch.
Print testMmatch'.

Definition testdef : Type -> Type := fun x=>x.
Lemma testret : Type -> Type.
MProof.
M.ret (fun x=>x).
Fail Qed. Abort.
Fail Print testret.

Polymorphic Lemma testexact : Type -> Type.
MProof.
T.exact (fun x=>x).
Qed.
About testexact.