1 files changed, 31 insertions, 0 deletions
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
new file mode 100644
index 00000000..c597f9bf
--- /dev/null
+++ b/test-suite/success/implicit.v
@@ -0,0 +1,31 @@
+(* Implicit on section variables *)
+
+Set Implicit Arguments.
+
+(* 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).
+
+(* Example submitted by Christine *)
+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.
+
+End Spec.
+
+(* Example submitted by Frédéric (interesting in v8 syntax) *)
+
+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)).
+(* V8 seulement 
+Check (fun x => @ rhs ? ? (f x)).
+*)