From ac27db8a4cdcc8f897e9580a832e0f3eb331cf6c Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 29 Oct 2009 11:19:28 +0000 Subject: Revision 12439 continued, printing part (notations to names behave like the name they refer to). Fixing buggy test-suite implicit.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12442 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/success/implicit.v | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'test-suite/success') diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index c6d0a6dd2..59e1a9352 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -14,6 +14,7 @@ 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}. @@ -21,7 +22,7 @@ Check (forall (type : Set) (elt : type) (empty : type -> bool), empty elt = true -> stack). -(* Nested sections and manual implicit arguments *) +(* Nested sections and manual/automatic implicit arguments *) Variable op' : forall A : Set, A -> A -> Set. Variable op'' : forall A : Set, A -> A -> Set. @@ -60,10 +61,6 @@ Check (eq1 0 0). Check (eq2 0 0). Check (eq3 nat 0 0). -(* Test discharge on automatic implicit arguments *) - -Check (op' 0 0). - (* Example submitted by Frédéric (interesting in v8 syntax) *) Parameter f : nat -> nat * nat. -- cgit v1.2.3