From f2132de33ab816360f60ec50ba124a685cdb942a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 28 Feb 2004 13:17:46 +0000
Subject: Exemple de Frederic

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5399 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/implicit.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 00230bfc46..9f2837e373 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -17,3 +17,13 @@ Record stack : Type := {type : Set; elt : type;
 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)).
+Check [x](!rhs ? ? (f x)).
-- 
cgit v1.2.3