Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

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').