diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-09 18:53:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-08-18 18:56:39 +0200 |
| commit | efa1c32a4d17870794dbc6f0301c3c0d46637a55 (patch) | |
| tree | 235cb1903dc5ffdd2ad4bdb7d3bc9cfc58e10de2 /pretyping/unification.ml | |
| parent | 5dcafa956e49eefc451dd021a0fe8ad2e2338088 (diff) | |
Fixing unification of subterms identified by patterns.
Diffstat (limited to 'pretyping/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f04a7294f..ed01c6b7b 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1228,12 +1228,8 @@ let make_pattern_test inf_flags env sigma0 (sigma,c) = | e when Errors.noncritical e -> raise (NotUnifiable None) in let merge_fun c1 c2 = match c1, c2 with - | Some (evd,c1), Some (_,c2) -> - (try let evd = w_typed_unify env evd Reduction.CONV flags c1 c2 in - Some (evd, c1) - with - | PretypeError (_,_,CannotUnify (c1,c2,Some e)) -> raise (NotUnifiable (Some (c1,c2,e))) - | e when Errors.noncritical e -> raise (NotUnifiable None)) + | Some (evd,c1) as x, Some (_,c2) -> + if is_conv env sigma c1 c2 then x else raise (NotUnifiable None) | Some _, None -> c1 | None, Some _ -> c2 | None, None -> None in |