diff options
author | 2000-09-12 11:02:30 +0000 | |
---|---|---|
committer | 2000-09-12 11:02:30 +0000 | |
commit | 6fcd224c128ae5e81f4cce9d5de1ac45883cfebf (patch) | |
tree | 9d5c886b18ca44f3a24de7b58c7dd7ca8bc88eec /kernel/inductive.ml | |
parent | 9248485d71d1c9c1796a22e526e07784493e2008 (diff) |
Modification mkAppL; abstraction via kind_of_term; changement dans Reduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
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 569b681e9..2f5e02ad4 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 *) |