diff options
| author | Hugo Herbelin | 2016-02-12 21:34:27 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-09 15:38:49 +0200 |
| commit | c2a9cf2730e5e2d7296449ad0acb406e25aead7f (patch) | |
| tree | e4e63eb044a0c1b5fd4c8741fba33f4e2d9a90f4 /pretyping | |
| parent | b9a15a390f34208bd642b0a97a35d32d3b3dfc01 (diff) | |
Minor simplification in evarconv.ml.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 17 |
1 files changed, 7 insertions, 10 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b8d92b9be7..fc22b6cb1e 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -318,25 +318,22 @@ 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, e = + let 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) + if b then Success evd + else UnifFailure (evd, ConversionFailed (env,term1,term2)) + with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) in match e with - | None -> Some (evd, e) - | Some e -> - if is_ground_env evd env then Some (evd, Some e) - else None) + | UnifFailure (evd, e) when not (is_ground_env evd env) -> None + | _ -> Some e) else None in match ground_test with - | Some (evd, None) -> Success evd - | Some (evd, Some e) -> UnifFailure (evd,e) + | Some result -> result | None -> (* Until pattern-unification is used consistently, use nohdbeta to not destroy beta-redexes that can be used for 1st-order unification *) |