diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 569b681e9a..2f5e02ad43 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -182,29 +182,29 @@ let ith_constructor_of_inductive (ind_sp,args) i = ((ind_sp,i),args) exception Induc let extract_mrectype t = - let (t,l) = whd_stack t [] in - match t with - | DOPN(MutInd ind_sp,args) -> ((ind_sp,args),l) + let (t, l) = whd_stack t in + match kind_of_term t with + | IsMutInd ind -> (ind, l) | _ -> raise Induc let find_mrectype env sigma c = - let (t,l) = whd_betadeltaiota_stack env sigma c [] in - match t with - | DOPN(MutInd ind_sp,args) -> ((ind_sp,args),l) + let (t, l) = whd_betadeltaiota_stack env sigma c in + match kind_of_term t with + | IsMutInd ind -> (ind, l) | _ -> raise Induc let find_minductype env sigma c = - let (t,l) = whd_betadeltaiota_stack env sigma c [] in - match t with - | DOPN(MutInd (sp,i),_) - when mind_type_finite (lookup_mind sp env) i -> (destMutInd t,l) + let (t, l) = whd_betadeltaiota_stack env sigma c in + match kind_of_term t with + | IsMutInd ((sp,i),_ as ind) + when mind_type_finite (lookup_mind sp env) i -> (ind, l) | _ -> raise Induc let find_mcoinductype env sigma c = - let (t,l) = whd_betadeltaiota_stack env sigma c [] in - match t with - | DOPN(MutInd (sp,i),_) - when not (mind_type_finite (lookup_mind sp env) i) -> (destMutInd t,l) + let (t, l) = whd_betadeltaiota_stack env sigma c in + match kind_of_term t with + | IsMutInd ((sp,i),_ as ind) + when not (mind_type_finite (lookup_mind sp env) i) -> (ind, l) | _ -> raise Induc (* raise Induc if not an inductive type *) |