1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
Unset Strict Universe Declaration.
Set Universe Polymorphism.
Set Printing Universes.
Record Cat := { Obj :> Type }.
Definition set_cat := {| Obj := Type |}.
Goal Type@{i} = Type@{j}.
Proof.
(* 1 subgoals
, subgoal 1 (ID 3)
============================
Type@{Top.368} = Type@{Top.370}
(dependent evars:) *)
let x := constr:(Type) in
let y := constr:(Obj set_cat) in
unify x y. (* success *)
let x := constr:(Type) in
let y := constr:(Obj set_cat) in
first [ unify x y | fail 2 "no unify" ];
change x with y at -1. (* Error: Not convertible. *)
reflexivity.
Defined.
|
