diff options
Diffstat (limited to 'test-suite')
| -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 c6d0a6dd2a..59e1a9352f 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. |