diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 37 |
1 files changed, 17 insertions, 20 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8e5faf01d5..68a60b16f4 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -964,26 +964,23 @@ let internalise sigma globalenv env allow_soapp lvar c = let tids = names_of_cases_indtype t in let tids = List.fold_right Idset.add tids Idset.empty in let t = intern_type (tids,None,scopes) t in - let (_,_,_,nal as indsign) = - match t with - | RRef (loc,IndRef ind) -> (loc,ind,0,[]) - | RApp (loc,RRef (_,IndRef ind),l) -> - let nparams, nrealargs = inductive_nargs globalenv ind in - let nindargs = nparams + nrealargs in - if List.length l <> nindargs then - error_wrong_numarg_inductive_loc loc globalenv ind nindargs; - let nal = List.map (function - | RHole _ -> Anonymous - | RVar (_,id) -> Name id - | c -> - user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in - let parnal,realnal = list_chop nparams nal in - if List.exists ((<>) Anonymous) parnal then - user_err_loc (loc,"", - str "The parameters of inductive type must be implicit"); - (loc,ind,nparams,realnal) - | _ -> error_bad_inductive_type (loc_of_rawconstr t) in - nal, Some indsign + let loc,ind,l = match t with + | RRef (loc,IndRef ind) -> (loc,ind,[]) + | RApp (loc,RRef (_,IndRef ind),l) -> (loc,ind,l) + | _ -> error_bad_inductive_type (loc_of_rawconstr t) in + let nparams, nrealargs = inductive_nargs globalenv ind in + let nindargs = nparams + nrealargs in + if List.length l <> nindargs then + error_wrong_numarg_inductive_loc loc globalenv ind nindargs; + let nal = List.map (function + | RHole _ -> Anonymous + | RVar (_,id) -> Name id + | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in + let parnal,realnal = list_chop nparams nal in + if List.exists ((<>) Anonymous) parnal then + user_err_loc (loc,"", + str "The parameters of inductive type must be implicit"); + realnal, Some (loc,ind,nparams,realnal) | None -> [], None in let na = match tm', na with |