diff options
Diffstat (limited to 'test-suite/success/Projection.v')
| -rw-r--r-- | test-suite/success/Projection.v | 27 |
1 files changed, 12 insertions, 15 deletions
diff --git a/test-suite/success/Projection.v b/test-suite/success/Projection.v index 7f5cd800..88da6013 100644 --- a/test-suite/success/Projection.v +++ b/test-suite/success/Projection.v @@ -1,10 +1,8 @@ -Structure S : Type := - {Dom : Type; - Op : Dom -> Dom -> Dom}. +Structure S : Type := {Dom : Type; Op : Dom -> Dom -> Dom}. -Check [s:S](Dom s). -Check [s:S](Op s). -Check [s:S;a,b:(Dom s)](Op s a b). +Check (fun s : S => Dom s). +Check (fun s : S => Op s). +Check (fun (s : S) (a b : Dom s) => Op s a b). (* v8 Check fun s:S => s.(Dom). @@ -13,17 +11,16 @@ Check fun (s:S) (a b:s.(Dom)) => s.(Op) a b. *) Set Implicit Arguments. -Unset Strict Implicits. +Unset Strict Implicit. +Unset Strict Implicit. -Structure S' [A:Set] : Type := - {Dom' : Type; - Op' : A -> Dom' -> Dom'}. +Structure S' (A : Set) : Type := {Dom' : Type; Op' : A -> Dom' -> Dom'}. -Check [s:(S' nat)](Dom' s). -Check [s:(S' nat)](Op' 2!s). -Check [s:(S' nat)](!Op' nat s). -Check [s:(S' nat);a:nat;b:(Dom' s)](Op' a b). -Check [s:(S' nat);a:nat;b:(Dom' s)](!Op' nat s a b). +Check (fun s : S' nat => Dom' s). +Check (fun s : S' nat => Op' (s:=s)). +Check (fun s : S' nat => Op' (A:=nat) (s:=s)). +Check (fun (s : S' nat) (a : nat) (b : Dom' s) => Op' a b). +Check (fun (s : S' nat) (a : nat) (b : Dom' s) => Op' (A:=nat) (s:=s) a b). (* v8 Check fun s:S' => s.(Dom'). |