diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 1 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 2 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 8 | ||||
| -rw-r--r-- | pretyping/typing.ml | 7 |
4 files changed, 12 insertions, 6 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index aa1c23f52..0dd3c5944 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1427,6 +1427,7 @@ and match_current pb (initial,tomatch) = let case = make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals in + let _ = Evarutil.evd_comb1 (Typing.type_of pb.env) pb.evdref pred in Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; { uj_val = applist (case, inst); uj_type = prod_applist !(pb.evdref) typ inst } diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index aefae1ecc..8afb9b942 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -929,7 +929,7 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_ with Not_found -> match expand_alias_once evd aliases t with | None -> raise Not_found - | Some c -> aux k c in + | Some c -> aux k (lift k c) in try let c = aux 0 c_in_env_extended_with_k_binders in Invertible (UniqueProjection (c,!effects)) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 71a457280..8ecec30cf 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -269,8 +269,9 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function | GCases (_,rtntypopt,tml,pl) -> let fold_pattern acc {v=(idl,p,c)} = f (List.fold_right g idl v) acc c in let fold_tomatch (v',acc) (tm,(na,onal)) = - (Option.fold_left (fun v'' {v=(_,nal)} -> List.fold_right (Name.fold_right g) nal v'') - (Name.fold_right g na v') onal, + ((if rtntypopt = None then v' else + Option.fold_left (fun v'' {v=(_,nal)} -> List.fold_right (Name.fold_right g) nal v'') + (Name.fold_right g na v') onal), f v acc tm) in let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in let acc = Option.fold_left (f v') acc rtntypopt in @@ -281,6 +282,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function | GIf (c,rtntyp,b1,b2) -> f v (f v (f v (fold_return_type_with_binders f g v acc rtntyp) c) b1) b2 | GRec (_,idl,bll,tyl,bv) -> + let v' = Array.fold_right g idl v in let f' i acc fid = let v,acc = List.fold_left @@ -288,7 +290,7 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function (Name.fold_right g na v, f v (Option.fold_left (f v) acc bbd) bty)) (v,acc) bll.(i) in - f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in + f v' (f v acc tyl.(i)) (bv.(i)) in Array.fold_left_i f' acc idl | GCast (c,k) -> let acc = match k with diff --git a/pretyping/typing.ml b/pretyping/typing.ml index bffe36eea..cf34ac016 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -197,10 +197,13 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj = (* FIXME: might depend on the level of actual parameters!*) let check_allowed_sort env sigma ind c p = - let pj = Retyping.get_judgment_of env sigma p in - let ksort = Sorts.family (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in let specif = Global.lookup_inductive (fst ind) in let sorts = elim_sorts specif in + let pj = Retyping.get_judgment_of env sigma p in + let _, s = splay_prod env sigma pj.uj_type in + let ksort = match EConstr.kind sigma s with + | Sort s -> Sorts.family (ESorts.kind sigma s) + | _ -> error_elim_arity env sigma ind sorts c pj None in if not (List.exists ((==) ksort) sorts) then let s = inductive_sort_family (snd specif) in error_elim_arity env sigma ind sorts c pj |