diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8d6a92a2..c8faf911 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrintern.ml 11739 2009-01-02 19:33:19Z herbelin $ *) +(* $Id: constrintern.ml 13131 2010-06-13 18:45:17Z herbelin $ *) open Pp open Util @@ -450,8 +450,8 @@ let rec simple_adjust_scopes n = function let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) = let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in let npar = mib.Declarations.mind_nparams in - snd (list_chop (List.length pl1 + npar) - (simple_adjust_scopes (npar + List.length pl2) + snd (list_chop (npar + List.length pl1) + (simple_adjust_scopes (npar + List.length pl1 + List.length pl2) (find_arguments_scope (ConstructRef cstr)))) (**********************************************************************) @@ -526,6 +526,7 @@ let error_invalid_pattern_notation loc = let chop_aconstr_constructor loc (ind,k) args = let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in + if nparams > List.length args then error_invalid_pattern_notation loc; let params,args = list_chop nparams args in List.iter (function AHole _ -> () | _ -> error_invalid_pattern_notation loc) params; @@ -728,8 +729,7 @@ let locate_if_isevar loc na = function let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) = if List.mem id indnames then errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++ - pr_id id ++ strbrk " must not be used as a bound variable in the type \ -of its constructor.") + pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") let push_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) = function | Anonymous -> @@ -1060,15 +1060,17 @@ let internalise sigma globalenv env allow_patvar lvar c = | CLetTuple (loc, nal, (na,po), b, c) -> let env' = reset_tmp_scope env in let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in - let env'' = List.fold_left (push_name_env lvar) env ids in - let p' = Option.map (intern_type env'') po in + let p' = Option.map (fun p -> + let env'' = List.fold_left (push_name_env lvar) env ids in + intern_type env'' p) po in RLetTuple (loc, nal, (na', p'), b', intern (List.fold_left (push_name_env lvar) env nal) c) | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in - let env'' = List.fold_left (push_name_env lvar) env ids in - let p' = Option.map (intern_type env'') po in + let p' = Option.map (fun p -> + let env'' = List.fold_left (push_name_env lvar) env ids in + intern_type env'' p) po in RIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole (loc, k) -> RHole (loc, match k with Some k -> k | None -> Evd.QuestionMark (Evd.Define true)) @@ -1147,6 +1149,7 @@ let internalise sigma globalenv env allow_patvar lvar c = [], None in let na = match tm', na with | RVar (_,id), None when Idset.mem id vars -> Name id + | RRef (loc, VarRef id), None -> Name id | _, None -> Anonymous | _, Some na -> na in (tm',(na,typ)), na::ids |