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

2 files changed, 11 insertions, 2 deletions

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