diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-07 15:55:56 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-07 15:55:56 +0100 |
| commit | a15ae330fd156b74fcdfb4fc39b79013d3e398bf (patch) | |
| tree | df52975748b4e5737385589788482ad057d1e937 /kernel/reduction.ml | |
| parent | 972c0e941a8acdd33053e2032ae0401b9aa4605d (diff) | |
| parent | e849572cd2b242b34fbec6c3eaa42e7d2e7cc550 (diff) | |
Merge PR #6685: Use whd-all on rigid-flex conversion.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index ecfca9057..1724f210d 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -468,7 +468,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (FFlex fl1, c2) -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv + (** By virtue of the previous case analyses, we know [c2] is rigid. + Conversion check to rigid terms eventually implies full weak-head + reduction, so instead of repeatedly performing small-step + unfoldings, we perform reduction with all flags on. *) + let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in + let r1 = whd_stack (infos_with_reds infos all) def1 v1 in + eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv | None -> match c2 with | FConstruct ((ind2,j2),u2) -> @@ -482,7 +488,10 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (c1, FFlex fl2) -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv + (** Symmetrical case of above. *) + let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in + let r2 = whd_stack (infos_with_reds infos all) def2 v2 in + eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv | None -> match c1 with | FConstruct ((ind1,j1),u1) -> |