diff options
Diffstat (limited to 'test-suite/prerequisite')
| -rw-r--r-- | test-suite/prerequisite/make_local.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/prerequisite/make_local.v b/test-suite/prerequisite/make_local.v index cdb7a2691..8700a6c4e 100644 --- a/test-suite/prerequisite/make_local.v +++ b/test-suite/prerequisite/make_local.v @@ -5,6 +5,6 @@ Definition f (A:Type) (a:A) := a. Local Arguments Scope f [type_scope type_scope]. Local Implicit Arguments f [A]. -(* Used in Import.v to test the locality flag *) +(* Used in ImportedCoercion.v to test the locality flag *) Local Coercion g (b:bool) := if b then 0 else 1. |