diff options
| author | Gaëtan Gilbert | 2018-10-02 16:13:31 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 15:46:16 +0100 |
| commit | 456919dd31f2f4bda15c6b37e4f1217bc085fc41 (patch) | |
| tree | a21b255f9bb570b4df07885c894243e2481c000d /kernel | |
| parent | f3c1fe8bc7979cd7036fcd2a1b2fe8f0a1acb058 (diff) | |
Switch order eqappr/check relevance in conversion.
This takes advantage of the mutability of the fconstr relevance mark.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/reduction.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index f32531721c..8c364602e9 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -329,9 +329,8 @@ let is_irrelevant infos lft c = (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = - if is_irrelevant infos lft1 term1 && is_irrelevant infos lft2 term2 - then cuniv - else eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv + try eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv + with NotConvertible when is_irrelevant infos lft1 term1 && is_irrelevant infos lft2 term2 -> cuniv (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *) and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = |