From f5c65bb6ff3d20dbec5b672b996b42a9e3a36697 Mon Sep 17 00:00:00 2001
From: pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 14 Jun 2012 22:16:32 +0000
Subject: Constrextern is allow to use partially applied notations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15440 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Notations.out | 9 +++++++--
 test-suite/output/Notations.v   | 4 ++++
 2 files changed, 11 insertions(+), 2 deletions(-)

(limited to 'test-suite/output')

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 5a32cff96..28621ccd8 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -116,9 +116,14 @@ fun x : option Z => match x with
                     end
      : option Z -> Z
 fun x : option Z => match x with
-                    | SOME3 _ x0 => x0
-                    | NONE3 _ => 0
+                    | SOME2 x0 => x0
+                    | NONE2 => 0
                     end
      : option Z -> Z
+fun x : list ?99 => match x with
+                    | NIL => NONE2
+                    | (_ :') t => SOME2 t
+                    end
+     : list ?99 -> option (list ?99)
 s
      : s
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index e560aecd8..d5763022e 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -246,6 +246,10 @@ Notation NONE3 := @None.
 Notation SOME3 := @Some.     
 Check (fun x => match x with SOME3 _ x => x | NONE3 _ => 0 end).
 
+Notation "a :'" := (cons a) (at level 12).
+
+Check (fun x => match x with | nil => NONE | h :' t => SOME3 _ t end).
+
 (* Check correct matching of "Type" in notations. Of course the
    notation denotes a term that will be reinterpreted with a different
    universe than the actual one; but it would be the same anyway
-- 
cgit v1.2.3