diff options
-rw-r--r-- | kernel/context.ml | 2 | ||||
-rw-r--r-- | kernel/reduction.ml | 88 | ||||
-rw-r--r-- | kernel/term_typing.ml | 5 |
3 files changed, 50 insertions, 45 deletions
diff --git a/kernel/context.ml b/kernel/context.ml index 6b5a6cdb9..e43e08865 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -80,7 +80,7 @@ let rel_context_tags ctx = let rec aux l = function | [] -> l | (_,Some _,_)::ctx -> aux (true::l) ctx - | (_,None _,_)::ctx -> aux (false::l) ctx + | (_,None,_)::ctx -> aux (false::l) ctx in aux [] ctx (*s Signatures of named hypotheses. Used for section variables and diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 9a7146890..64964f85e 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -370,24 +370,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | Some (def2,s2) -> eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv | None -> - if Projection.equal p1 p2 && compare_stack_shape v1 v2 then + if Constant.equal (Projection.constant p1) (Projection.constant p2) + && compare_stack_shape v1 v2 then let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 u1 - else (* Two projections in WHNF: unfold *) - raise NotConvertible) + else raise NotConvertible) - | (FProj (p1,c1), t2) -> - (match unfold_projection infos p1 c1 with - | Some (def1,s1) -> - eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv - | None -> raise NotConvertible) - - | (_, FProj (p2,c2)) -> - (match unfold_projection infos p2 c2 with - | Some (def2,s2) -> - eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv - | None -> raise NotConvertible) - (* other constructors *) | (FLambda _, FLambda _) -> (* Inconsistency: we tolerate that v1, v2 contain shift and update but @@ -428,31 +416,53 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* only one constant, defined var or defined rel *) | (FFlex fl1, c2) -> - (match unfold_reference infos fl1 with - | Some def1 -> - eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv - | None -> - match c2 with - | FConstruct ((ind2,j2),u2) -> - (try - let v2, v1 = - eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1) - in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - with Not_found -> raise NotConvertible) - | _ -> raise NotConvertible) - + (match unfold_reference infos fl1 with + | Some def1 -> + eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv + | None -> + match c2 with + | FConstruct ((ind2,j2),u2) -> + (try + let v2, v1 = + eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1) + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + with Not_found -> raise NotConvertible) + | FProj (p2,c2) -> + (match unfold_projection infos p2 c2 with + | Some (def2,s2) -> + eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv + | None -> raise NotConvertible) + | _ -> raise NotConvertible) + | (c1, FFlex fl2) -> - (match unfold_reference infos fl2 with - | Some def2 -> - eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv - | None -> - match c1 with - | FConstruct ((ind1,j1),u1) -> - (try let v1, v2 = - eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2) - in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - with Not_found -> raise NotConvertible) - | _ -> raise NotConvertible) + (match unfold_reference infos fl2 with + | Some def2 -> + eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv + | None -> + match c1 with + | FConstruct ((ind1,j1),u1) -> + (try let v1, v2 = + eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2) + in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv + with Not_found -> raise NotConvertible) + | FProj (p1,c1) -> + (match unfold_projection infos p1 c1 with + | Some (def1,s1) -> + eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv + | None -> raise NotConvertible) + | _ -> raise NotConvertible) + + | (FProj (p1,c1), t2) -> + (match unfold_projection infos p1 c1 with + | Some (def1,s1) -> + eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv + | None -> raise NotConvertible) + + | (t1, FProj (p2,c2)) -> + (match unfold_projection infos p2 c2 with + | Some (def2,s2) -> + eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv + | None -> raise NotConvertible) (* Inductive types: MutInd MutConstruct Fix Cofix *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 8f41f356d..79b3d518a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -65,11 +65,6 @@ let handle_side_effects env body side_eff = | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub c i x) i x in let rec sub_body c u b i x = match kind_of_term x with | Const (c',u') when eq_constant c c' -> - (* let subst = *) - (* Array.fold_left2 (fun subst l l' -> Univ.LMap.add l l' subst) *) - (* Univ.LMap.empty (Instance.to_array u) (Instance.to_array u') *) - (* in *) - (* Vars.subst_univs_level_constr subst b *) Vars.subst_instance_constr u' b | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in let fix_body (c,cb,b) t = |