diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-26 15:50:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-26 15:50:20 +0000 |
| commit | 9b05df26c99fcdddb41d9ef1e9dc3b0571b9395b (patch) | |
| tree | 74761c53f38c617c6bdfcbbd9d187683aad0453e /test-suite/prerequisite | |
| parent | 80d0def3cd49c16a989b61b74232868578c96a03 (diff) | |
Local/Global revision 12418 continued
- Fixing non-export of newly created Local Argument Scope.
- Fixing bad discharge of local variables in nested sections
(bug still exists in v8.2).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12420 85f007b7-540e-0410-9357-904b9bb8a0f7
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. |