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
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
Require Import Program.Tactics.
Set Universe Polymorphism.
Module Bug11766.
Program Definition bla@{} : nat := _.
Next Obligation.
let x := constr:(Type) in exact 0.
Defined. (* was unbound univ *)
Program Definition bla'@{} : nat := _.
Solve Obligations with let x := constr:(Type) in exact 0. (* was unbound univ *)
End Bug11766.
From Coq Require Import ssreflect.
Module Bug11988.
#[local]
Obligation Tactic := idtac.
Section Foo.
Universe u.
Variable T : Type@{u}.
Variable op : T -> T -> T.
Hypothesis opC : forall x y, op x y = op y x.
Program Definition foo@{} x y : {z : T & z = op x y} :=
existT _ (op y x) _.
Next Obligation.
move=> /= x y.
by rewrite -[RHS]opC.
Qed. (* should work even though rewrite [RHS] adds a spurious universe *)
End Foo.
End Bug11988.
Module ExampleFrom11902.
Local Unset Universe Polymorphism.
Program Definition foo (X : Type) : Type :=
let x := X in forall x : x, _.
Next Obligation.
refine nat.
Defined.
End ExampleFrom11902.
|
