diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-13 16:04:10 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-13 16:04:10 +0000 |
| commit | 5073e2712725b54c928c7438e3215e89c4e627fc (patch) | |
| tree | c30978ec198c89fc41230d5bedc21294be38df34 | |
| parent | 961672aa25747fb277fa60eae99ca8d82b0e0fc6 (diff) | |
Niveau V8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4894 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | test-suite/success/implicit.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index f767e80a9..00230bfc4 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -7,7 +7,7 @@ Set Implicit Arguments. Section Spec. Variable A:Set. Variable op : (A:Set)A->A->Set. -Infix 6 "#" op. +Infix 6 "#" op V8only (at level 70). Check (x:A)(x # x). (* Example submitted by Christine *) |