blob: 6d9117c05cb5fdea44289df163195bd546c37ca8 (
plain)
1
2
3
4
5
6
7
8
9
|
(* Used in Import.v to test the locality flag *)
Definition f (A:Type) (a:A) := a.
Local Arguments f [A]%type_scope _%type_scope.
(* Used in ImportedCoercion.v to test the locality flag *)
Local Coercion g (b:bool) := if b then 0 else 1.
|
