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/evarconv.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/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 23 |
1 files changed, 15 insertions, 8 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 616ceeabdc..f388f90057 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -324,18 +324,25 @@ let rec evar_conv_x ts env evd pbty term1 term2 = Note: incomplete heuristic... *) let ground_test = if is_ground_term evd term1 && is_ground_term evd term2 then ( - let evd, b = - try infer_conv ~pb:pbty ~ts:(fst ts) env evd term1 term2 - with Univ.UniverseInconsistency _ -> evd, false + let evd, e = + try + let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) + env evd term1 term2 + in + if b then evd, None + else evd, Some (ConversionFailed (env,term1,term2)) + with Univ.UniverseInconsistency e -> evd, Some (UnifUnivInconsistency e) in - if b then Some (evd, true) - else if is_ground_env evd env then Some (evd, false) - else None) + match e with + | None -> Some (evd, e) + | Some e -> + if is_ground_env evd env then Some (evd, Some e) + else None) else None in match ground_test with - | Some (evd, true) -> Success evd - | Some (evd, false) -> UnifFailure (evd,ConversionFailed (env,term1,term2)) + | Some (evd, None) -> Success evd + | Some (evd, Some e) -> UnifFailure (evd,e) | None -> (* Until pattern-unification is used consistently, use nohdbeta to not destroy beta-redexes that can be used for 1st-order unification *) |