diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
| commit | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (patch) | |
| tree | 12e8931a4a56da1a1bdfb89d670f4ba38fe08e1f /pretyping/evarconv.ml | |
| parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) | |
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 26 |
1 files changed, 16 insertions, 10 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a95af253..f388f900 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 *) @@ -555,8 +562,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | LetIn (na,b1,t1,c'1), LetIn (_,b2,t2,c'2) -> let f1 i = ise_and i - [(fun i -> evar_conv_x ts env i CONV t1 t2); - (fun i -> evar_conv_x ts env i CONV b1 b2); + [(fun i -> evar_conv_x ts env i CONV b1 b2); (fun i -> let b = nf_evar i b1 in let t = nf_evar i t1 in |