diff options
| author | Matthieu Sozeau | 2014-09-05 16:52:38 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-05 16:53:56 +0200 |
| commit | 901ff5c7cb30165ccf5a8e8d62eb3e775d3e962c (patch) | |
| tree | d6a68322929e833aae615e4cefb698f42f81b7ad /kernel/reduction.ml | |
| parent | 581cbe36191901f1dc234fe77d619abfe7b8de34 (diff) | |
Rename eta_expand_ind_stacks, fix the one from the checker and adapt
it to the new representation of projections and the new mind_finite
type.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 78d2105ab0..ebba231654 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -434,7 +434,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | FConstruct ((ind2,j2),u2) -> (try let v2, v1 = - eta_expand_ind_stacks (info_env infos) ind2 hd2 v2 (snd appr1) + 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) @@ -447,7 +447,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = match c1 with | FConstruct ((ind1,j1),u1) -> (try let v1, v2 = - eta_expand_ind_stacks (info_env infos) ind1 hd1 v1 (snd appr2) + 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) @@ -472,14 +472,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FConstruct ((ind1,j1),u1), _) -> (try let v1, v2 = - eta_expand_ind_stacks (info_env infos) ind1 hd1 v1 (snd appr2) + 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) | (_, FConstruct ((ind2,j2),u2)) -> (try let v2, v1 = - eta_expand_ind_stacks (info_env infos) ind2 hd2 v2 (snd appr1) + 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) |