diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-29 11:19:28 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-29 11:19:28 +0000 |
| commit | ac27db8a4cdcc8f897e9580a832e0f3eb331cf6c (patch) | |
| tree | c77083c17c8f0dd6bfb150a964f78fa32d035f53 /test-suite/success/implicit.v | |
| parent | 815d4dc9ccc2938859c22b5848d153c50fee0192 (diff) | |
Revision 12439 continued, printing part (notations to names behave
like the name they refer to).
Fixing buggy test-suite implicit.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12442 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/implicit.v')
| -rw-r--r-- | test-suite/success/implicit.v | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index c6d0a6dd2..59e1a9352 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -14,6 +14,7 @@ Infix "#" := op (at level 70). Check (forall x : A, x # x). (* Example submitted by Christine *) + Record stack : Type := {type : Set; elt : type; empty : type -> bool; proof : empty elt = true}. @@ -21,7 +22,7 @@ Check (forall (type : Set) (elt : type) (empty : type -> bool), empty elt = true -> stack). -(* Nested sections and manual implicit arguments *) +(* Nested sections and manual/automatic implicit arguments *) Variable op' : forall A : Set, A -> A -> Set. Variable op'' : forall A : Set, A -> A -> Set. @@ -60,10 +61,6 @@ 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. |