aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/7421.v
blob: afcdd35fccee432846edb703dbf99d310ba47d3e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39


Universe i j.

Goal False.
Proof.
  Check Type@{i} : Type@{j}.
  Fail constr_eq_strict Type@{i} Type@{j}.
  assert_succeeds constr_eq Type@{i} Type@{j}. (* <- i=j is forgotten after assert_succeeds *)
  Fail constr_eq_strict Type@{i} Type@{j}.

  constr_eq Type@{i} Type@{j}. (* <- i=j is retained *)
  constr_eq_strict Type@{i} Type@{j}.
  Fail Check Type@{i} : Type@{j}.

  Fail constr_eq Prop Set.
  Fail constr_eq Prop Type.

  Fail constr_eq_strict Type Type.
  constr_eq Type Type.

  constr_eq_strict Set Set.
  constr_eq Set Set.
  constr_eq Prop Prop.

  let x := constr:(Type) in constr_eq_strict x x.
  let x := constr:(Type) in constr_eq x x.

  Fail lazymatch type of prod with
       | ?A -> ?B -> _ => constr_eq_strict A B
       end.
  lazymatch type of prod with
  | ?A -> ?B -> _ => constr_eq A B
  end.
  lazymatch type of prod with
  | ?A -> ?B -> ?C => constr_eq A C
  end.

Abort.