diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 15:27:10 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-14 15:27:10 +0200 |
| commit | a3c40242a4786afd86cbfce7208e7b42b09c0863 (patch) | |
| tree | af2ed94c35f780507e4fcf5ae1164c00e3a9923e | |
| parent | dcc5064bbc6f01b498abfdf80f0ea13a26381926 (diff) | |
| parent | 256ca51bafc7200c8c006981cad60e57014e0dbc (diff) | |
Merge PR#448: Do not recompute twice the whnf of terms in conversion.
| -rw-r--r-- | kernel/reduction.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 427ce04c5..b6786c045 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -356,17 +356,17 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let (app1,app2) = if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then match unfold_reference infos fl1 with - | Some def1 -> ((lft1, whd def1 v1), appr2) + | Some def1 -> ((lft1, (def1, v1)), appr2) | None -> (match unfold_reference infos fl2 with - | Some def2 -> (appr1, (lft2, whd def2 v2)) + | Some def2 -> (appr1, (lft2, (def2, v2))) | None -> raise NotConvertible) else match unfold_reference infos fl2 with - | Some def2 -> (appr1, (lft2, whd def2 v2)) + | Some def2 -> (appr1, (lft2, (def2, v2))) | None -> (match unfold_reference infos fl1 with - | Some def1 -> ((lft1, whd def1 v1), appr2) + | Some def1 -> ((lft1, (def1, v1)), appr2) | None -> raise NotConvertible) in eqappr cv_pb l2r infos app1 app2 cuniv) @@ -377,11 +377,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = form *) (match unfold_projection infos p1 c1 with | Some (def1,s1) -> - eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, s1 :: v1)) appr2 cuniv | None -> match unfold_projection infos p2 c2 with | Some (def2,s2) -> - eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, s2 :: v2)) cuniv | None -> if Constant.equal (Projection.constant p1) (Projection.constant p2) && compare_stack_shape v1 v2 then @@ -393,26 +393,26 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (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 + eqappr cv_pb l2r infos (lft1, (def1, s1 :: v1)) appr2 cuniv | None -> (match t2 with | FFlex fl2 -> (match unfold_reference infos fl2 with | Some def2 -> - eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv | None -> raise NotConvertible) | _ -> 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 + eqappr cv_pb l2r infos appr1 (lft2, (def2, s2 :: v2)) cuniv | None -> (match t1 with | FFlex fl1 -> (match unfold_reference infos fl1 with | Some def1 -> - eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv | None -> raise NotConvertible) | _ -> raise NotConvertible)) @@ -458,7 +458,7 @@ 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, whd def1 v1) appr2 cuniv + eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv | None -> match c2 with | FConstruct ((ind2,j2),u2) -> @@ -472,7 +472,7 @@ 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, whd def2 v2) cuniv + eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv | None -> match c1 with | FConstruct ((ind1,j1),u1) -> |