diff options
| author | Matthieu Sozeau | 2018-06-05 12:11:22 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-06-05 12:11:22 +0200 |
| commit | f5a86aa6d18f569ac305559efd559ecad8f0b470 (patch) | |
| tree | cc6e4c5d852ee84dc99cf9f9024c76b2fda1acd9 /pretyping/reductionops.ml | |
| parent | af65c79cc976f3f96a768f3d0897febb24e1485a (diff) | |
| parent | d4dac391db9e3be7a45d26e2da9007997b79587d (diff) | |
Merge PR #7099: Stronger invariants in unification signature.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 20 |
1 files changed, 8 insertions, 12 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 6fde868370..7fb1a0a578 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1348,11 +1348,10 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = (** FIXME *) try - let b, sigma = - let ans = - if pb == Reduction.CUMUL then + let ans = match pb with + | Reduction.CUMUL -> EConstr.leq_constr_universes env sigma x y - else + | Reduction.CONV -> EConstr.eq_constr_universes env sigma x y in let ans = match ans with @@ -1362,20 +1361,17 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None in match ans with - | None -> false, sigma - | Some sigma -> true, sigma - in - if b then sigma, true - else + | Some sigma -> ans + | None -> let x = EConstr.Unsafe.to_constr x in let y = EConstr.Unsafe.to_constr y in let sigma' = conv_fun pb ~l2r:false sigma ts env (sigma, sigma_univ_state) x y in - sigma', true + Some sigma' with - | Reduction.NotConvertible -> sigma, false - | Univ.UniverseInconsistency _ when catch_incon -> sigma, false + | Reduction.NotConvertible -> None + | Univ.UniverseInconsistency _ when catch_incon -> None | e when is_anomaly e -> report_anomaly e let infer_conv = infer_conv_gen (fun pb ~l2r sigma -> |