From f5c65bb6ff3d20dbec5b672b996b42a9e3a36697 Mon Sep 17 00:00:00 2001
From: pboutill
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
---
 interp/notation_ops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 853c6967c1..b1067fa473 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -756,7 +756,7 @@ let rec match_cases_pattern metas sigma a1 a2 =
       when r1 = r2 ->
       let l1 = add_patterns_for_params (fst r1) args1 in
       let le2 = List.length l2 in
-      if le2 > List.length l1
+      if le2 = 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1
       then
 	raise No_match
       else
@@ -779,7 +779,7 @@ let match_ind_pattern metas sigma ind pats a2 =
   | NApp (NRef (IndRef r2),l2)
       when ind = r2 ->
       let le2 = List.length l2 in
-      if le2 > List.length pats
+      if le2 = 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats
       then
 	raise No_match
       else
-- 
cgit v1.2.3