diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 62aa9a2d7b..722705bd70 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -38,14 +38,14 @@ let find_inductive env c = let (t, l) = decompose_app (whd_all env c) in match kind t with | Ind ind - when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l) + when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> CoFinite -> (ind, l) | _ -> raise Not_found let find_coinductive env c = let (t, l) = decompose_app (whd_all env c) in match kind t with | Ind ind - when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l) + when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == CoFinite -> (ind, l) | _ -> raise Not_found let inductive_params (mib,_) = mib.mind_nparams @@ -796,18 +796,18 @@ let rec subterm_specif renv stack t = | Proj (p, c) -> let subt = subterm_specif renv stack c in - (match subt with - | Subterm (s, wf) -> - (* We take the subterm specs of the constructor of the record *) - let wf_args = (dest_subterms wf).(0) in - (* We extract the tree of the projected argument *) - let kn = Projection.constant p in - let cb = lookup_constant kn renv.env in - let pb = Option.get cb.const_proj in - let n = pb.proj_arg in - Subterm (Strict, List.nth wf_args n) - | Dead_code -> Dead_code - | Not_subterm -> Not_subterm) + (match subt with + | Subterm (s, wf) -> + (* We take the subterm specs of the constructor of the record *) + let wf_args = (dest_subterms wf).(0) in + (* We extract the tree of the projected argument *) + let kn = Projection.constant p in + let cb = lookup_constant kn renv.env in + let pb = Option.get cb.const_proj in + let n = pb.proj_arg in + spec_of_tree (List.nth wf_args n) + | Dead_code -> Dead_code + | Not_subterm -> Not_subterm) | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _ | Construct _ | CoFix _ -> Not_subterm @@ -1098,8 +1098,8 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = () (* -let cfkey = Profile.declare_profile "check_fix";; -let check_fix env fix = Profile.profile3 cfkey check_fix env fix;; +let cfkey = CProfile.declare_profile "check_fix";; +let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;; *) (************************************************************************) |