diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
| commit | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (patch) | |
| tree | fbb91e2f74c73bb867ab62c58f248a704bbe6dec /interp/constrintern.ml | |
| parent | 6497f27021fec4e01f2182014f2bb1989b4707f9 (diff) | |
Imported Upstream version 8.0pl3upstream/8.0pl3
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 222ea23b..bacdb387 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrintern.ml,v 1.58.2.6 2004/11/22 14:21:23 herbelin Exp $ *) +(* $Id: constrintern.ml,v 1.58.2.7 2005/11/19 10:34:35 herbelin Exp $ *) open Pp open Util @@ -621,10 +621,10 @@ let merge_impargs l args = let check_projection isproj nargs r = match (r,isproj) with - | RRef (loc, ref), Some nth -> + | RRef (loc, ref), Some _ -> (try - let n = Recordops.find_projection_nparams ref in - if nargs < nth then + let n = Recordops.find_projection_nparams ref + 1 in + if nargs < n then user_err_loc (loc,"",str "Projection has not enough parameters"); with Not_found -> user_err_loc |