diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-24 16:48:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-09-24 16:48:05 +0000 |
| commit | 97187ce18aca111c0cb1d275eec33d20854a9b53 (patch) | |
| tree | b2a9e09526e2401afc4e40c2626a7caafa6fb811 | |
| parent | 00c942b5352b4b136802cfc92d36eb9512c4df21 (diff) | |
Correction bug dans détection clause "in" mal formée quand le "in" est
donné alors même qu'il n'est pas utile car ne lie aucun argument.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9173 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 8e5faf01d..68a60b16f 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 |