diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-05 16:52:38 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-05 16:53:56 +0200 |
| commit | 901ff5c7cb30165ccf5a8e8d62eb3e775d3e962c (patch) | |
| tree | d6a68322929e833aae615e4cefb698f42f81b7ad /checker/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 'checker/reduction.ml')
| -rw-r--r-- | checker/reduction.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml index 7bdc96283..403d27779 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -357,7 +357,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = | FConstruct ((ind2,j2),u2) -> (try let v2, v1 = - eta_expand_ind_stacks (infos_env infos) ind2 hd2 v2 (snd appr1) + eta_expand_ind_stack (infos_env infos) ind2 hd2 v2 (snd appr1) in convert_stacks univ infos lft1 lft2 v1 v2 with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) @@ -370,7 +370,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = match c1 with | FConstruct ((ind1,j1),u1) -> (try let v1, v2 = - eta_expand_ind_stacks (infos_env infos) ind1 hd1 v1 (snd appr2) + eta_expand_ind_stack (infos_env infos) ind1 hd1 v1 (snd appr2) in convert_stacks univ infos lft1 lft2 v1 v2 with Not_found -> raise NotConvertible) | _ -> raise NotConvertible) |