blob: f62f6109e144bb87b231b7fc6b5538b4496e78b0 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Section S.
Variable A : Type.
Fail Primitive int : let x := A in Set := #int63_type.
Fail Primitive add := #int63_add.
End S.
(* [Primitive] should be forbidden in sections, otherwise its type after cooking
will be incorrect:
Check int.
*)
|
