diff options
| author | pboutill | 2011-07-22 13:26:27 +0000 |
|---|---|---|
| committer | pboutill | 2011-07-22 13:26:27 +0000 |
| commit | 2145319442699bb3a2ab0158ea702fa2558a5150 (patch) | |
| tree | 9003e71012236a26a7aa8ea583f92ab8ad93de45 /interp/constrintern.ml | |
| parent | 3bc1612a8b3a7c5ab52c3cd68cc1670b916438c0 (diff) | |
Add a syntax entry for fully applied constructor pattern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14292 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 016f4a6584..7cca7347b7 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1045,7 +1045,7 @@ let rec intern_cases_pattern genv env (ids,asubst as aliases) pat = | Some (_, head, pl) -> CPatCstr(loc, head, pl) in intern_pat env aliases self_patt - | CPatCstr (loc, head, pl) -> + | CPatCstr (loc, head, pl) | CPatCstrExpl (loc, head, pl) -> let c,idslpl1,pl2 = mustbe_constructor loc head intern_pat aliases pl env in check_constructor_length genv loc c idslpl1 pl2; let argscs2 = find_remaining_constructor_scopes idslpl1 pl2 c in |