blob: 968ea71a94416715b072603391e6485910c38447 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(* Check that types are not uselessly unfolded *)
(* Check here that P returns something of type "option L" and not
"option (list nat)" *)
Definition L := list nat.
Definition P (e:option L) :=
match e with
| None => None
| Some cl => Some cl
end.
Print P.
|
