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/success/implicit.v | |
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/success/implicit.v')
-rw-r--r-- | test-suite/success/implicit.v | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index aabb057a4..c6d0a6dd2 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -1,3 +1,5 @@ +(* Testing the behavior of implicit arguments *) + (* Implicit on section variables *) Set Implicit Arguments. @@ -19,8 +21,49 @@ Check (forall (type : Set) (elt : type) (empty : type -> bool), empty elt = true -> stack). +(* Nested sections and manual implicit arguments *) + +Variable op' : forall A : Set, A -> A -> Set. +Variable op'' : forall A : Set, A -> A -> Set. + +Section B. + +Definition eq1 := fun (A:Type) (x y:A) => x=y. +Definition eq2 := fun (A:Type) (x y:A) => x=y. +Definition eq3 := fun (A:Type) (x y:A) => x=y. + +Implicit Arguments op' []. +Global Implicit Arguments op'' []. + +Implicit Arguments eq2 []. +Global Implicit Arguments eq3 []. + +Check (op 0 0). +Check (op' nat 0 0). +Check (op'' nat 0 0). +Check (eq1 0 0). +Check (eq2 nat 0 0). +Check (eq3 nat 0 0). + +End B. + +Check (op 0 0). +Check (op' 0 0). +Check (op'' nat 0 0). +Check (eq1 0 0). +Check (eq2 0 0). +Check (eq3 nat 0 0). + End Spec. +Check (eq1 0 0). +Check (eq2 0 0). +Check (eq3 nat 0 0). + +(* Test discharge on automatic implicit arguments *) + +Check (op' 0 0). + (* Example submitted by Frédéric (interesting in v8 syntax) *) Parameter f : nat -> nat * nat. |