diff options
| author | pboutill | 2012-06-14 22:16:32 +0000 |
|---|---|---|
| committer | pboutill | 2012-06-14 22:16:32 +0000 |
| commit | f5c65bb6ff3d20dbec5b672b996b42a9e3a36697 (patch) | |
| tree | 702ab96ec7ca174b3fa4437c3f43047b84172730 /interp/notation_ops.ml | |
| parent | b2953849b999d1c3b42c0f494b234f2a93ac7754 (diff) | |
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
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |