diff options
| author | Hugo Herbelin | 2015-01-03 15:44:03 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-01-03 16:06:18 +0100 |
| commit | 893a02f643858ba0b0172648e77af9ccb65f03df (patch) | |
| tree | e5b835376bdf3e00e073608bdc18346513059973 | |
| parent | 353b523c0c808d0650cd77821363b0c865aedecf (diff) | |
Tentatively trying to restore the use of second-order typed-based
unification algorithm in consider_remaining_unif_problems. If it
happens to be problematic, one can backtrack to the "optimization"
from 3bd9cb26b which has a restriction on rels/vars.
| -rw-r--r-- | pretyping/evarconv.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e906629508..a5d11fbfb1 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1062,13 +1062,11 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = with TypingFailed evd -> evd, false let second_order_matching_with_args ts env evd ev l t = -(* - let evd,ev = evar_absorb_arguments env evd ev l in + let evd,ev = evar_absorb_arguments env evd ev (Array.to_list l) in let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in let evd, b = second_order_matching ts env evd ev argoccs t in - if b then Success evd else -*) - UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) + if b then Success evd + else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in |