diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 22 | ||||
| -rw-r--r-- | pretyping/inferCumulativity.ml | 34 |
2 files changed, 19 insertions, 37 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 754e881398..18ecbf8ed3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -451,17 +451,15 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = then Anonymous, None, None else - match Option.map detype p with - | None -> Anonymous, None, None - | Some p -> - let nl,typ = it_destRLambda_or_LetIn_names k p in - let n,typ = match DAst.get typ with - | GLambda (x,_,t,c) -> x, c - | _ -> Anonymous, typ in - let aliastyp = - if List.for_all (Name.equal Anonymous) nl then None - else Some (Loc.tag (indsp,nl)) in - n, aliastyp, Some typ + let p = detype p in + let nl,typ = it_destRLambda_or_LetIn_names k p in + let n,typ = match DAst.get typ with + | GLambda (x,_,t,c) -> x, c + | _ -> Anonymous, typ in + let aliastyp = + if List.for_all (Name.equal Anonymous) nl then None + else Some (Loc.tag (indsp,nl)) in + n, aliastyp, Some typ in let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in let tag = @@ -650,7 +648,7 @@ and detype_r d flags avoid env sigma t = (is_nondep_branch sigma) avoid (ci.ci_ind,ci.ci_pp_info.style, ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags) - (Some p) c bl + p c bl | Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef | CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index a0a8276c5c..a4097237ff 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -159,34 +159,21 @@ and infer_vect infos variances v = let infer_term cv_pb env variances c = let open CClosure in - let reds = RedFlags.red_add_transparent betaiotazeta Names.full_transparent_state in - let infos = create_clos_infos reds env in + let infos = create_clos_infos all env in infer_fterm cv_pb infos variances (CClosure.inject c) [] -let infer_arity_constructor env variances arcn is_arity params = - let numchecked = ref 0 in - let numparams = Context.Rel.nhyps params in - let basic_check env variances tp = - let variances = - if !numchecked >= numparams then - infer_term CUMUL env variances tp - else - variances - in - numchecked := !numchecked + 1; variances - in +let infer_arity_constructor is_arity env variances arcn = let infer_typ typ (env,variances) = match typ with | Context.Rel.Declaration.LocalAssum (_, typ') -> - (Environ.push_rel typ env, basic_check env variances typ') + (Environ.push_rel typ env, infer_term CUMUL env variances typ') | Context.Rel.Declaration.LocalDef _ -> assert false in - let arcn' = Term.it_mkProd_or_LetIn arcn params in - let typs, codom = Reduction.dest_prod env arcn' in + let typs, codom = Reduction.dest_prod env arcn in let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j} i is irrelevant, j is invariant. *) - if not is_arity then basic_check env variances codom else variances + if not is_arity then infer_term CUMUL env variances codom else variances let infer_inductive env mie = let open Entries in @@ -205,15 +192,12 @@ let infer_inductive env mie = Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances) LMap.empty uarray in + let env, _ = Typeops.infer_local_decls env params in let variances = List.fold_left (fun variances entry -> - let _, params = Typeops.infer_local_decls env params in - let variances = infer_arity_constructor - env variances entry.mind_entry_arity true params + let variances = infer_arity_constructor true + env variances entry.mind_entry_arity in - List.fold_left - (fun variances cons -> - infer_arity_constructor - env variances cons false params) + List.fold_left (infer_arity_constructor false env) variances entry.mind_entry_lc) variances entries |