diff options
| author | Matthieu Sozeau | 2015-03-04 00:32:58 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-03-04 00:32:58 +0100 |
| commit | 85fc5f90c52a755d1b64640f4f0b3421979c0fe8 (patch) | |
| tree | af7c16aa9db83cb81a0994dfab3364cf0d50702b /pretyping/reductionops.ml | |
| parent | c35c97e7c904f2109110c64f2ba9e45e945de381 (diff) | |
Fix bug #3532, providing universe inconsistency information when a
unification fails due to that, during a conversion step.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 21f13a51f1..dd671f111e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1293,7 +1293,8 @@ let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; Reduction.compare_instances = sigma_compare_instances } -let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = +let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) + env sigma x y = try let b, sigma = let b, cstrs = @@ -1315,7 +1316,7 @@ let infer_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y sigma', true with | Reduction.NotConvertible -> sigma, false - | Univ.UniverseInconsistency _ -> sigma, false + | Univ.UniverseInconsistency _ when catch_incon -> sigma, false | e when is_anomaly e -> error "Conversion test raised an anomaly" (********************************************************************) |