From 893a02f643858ba0b0172648e77af9ccb65f03df Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 3 Jan 2015 15:44:03 +0100
Subject: 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.

---
 pretyping/evarconv.ml | 8 +++-----
 1 file 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
-- 
cgit v1.2.3