diff options
Diffstat (limited to 'test-suite/success/implicit.v')
| -rw-r--r-- | test-suite/success/implicit.v | 25 |
1 files changed, 14 insertions, 11 deletions
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index c597f9bf..1786424e 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -1,20 +1,23 @@ (* Implicit on section variables *) Set Implicit Arguments. +Unset Strict Implicit. (* Example submitted by David Nowak *) Section Spec. -Variable A:Set. -Variable op : (A:Set)A->A->Set. -Infix 6 "#" op V8only (at level 70). -Check (x:A)(x # x). +Variable A : Set. +Variable op : forall A : Set, A -> A -> Set. +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 }. +Record stack : Type := + {type : Set; elt : type; empty : type -> bool; proof : empty elt = true}. -Check (type:Set; elt:type; empty:(type->bool))(empty elt)=true->stack. +Check + (forall (type : Set) (elt : type) (empty : type -> bool), + empty elt = true -> stack). End Spec. @@ -22,10 +25,10 @@ End Spec. Parameter f : nat -> nat * nat. Notation lhs := fst. -Check [x](lhs ? ? (f x)). -Check [x](!lhs ? ? (f x)). -Notation "'rhs'" := snd. -Check [x](rhs ? ? (f x)). +Check (fun x => fst (f x)). +Check (fun x => fst (f x)). +Notation rhs := snd. +Check (fun x => snd (f x)). (* V8 seulement Check (fun x => @ rhs ? ? (f x)). *) |