From daae294d35dd3ea8655a989681944654087dbf97 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 22 Oct 2011 21:33:15 +0000
Subject: Use also second-order unification if first-order fails at the time of
 considering open problems

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14580 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarconv.ml | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 283363f37e..f399420255 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -684,6 +684,10 @@ let second_order_matching ts env_rhs evd (evk,args) rhs =
   abstract_free_holes evd subst, true
   with Exit -> 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
+  second_order_matching ts env evd ev 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
   let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in
@@ -702,18 +706,24 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       choose_less_dependent_instance evk2 evd term1 args2, true
   | Evar ev1,_ when List.length l1 <= List.length l2 ->
       (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
-      first_order_unification ts env evd (ev1,l1) appr2
+      (* and otherwise second-order matching *)
+      ise_try evd
+        [(fun evd -> first_order_unification ts env evd (ev1,l1) appr2);
+         (fun evd ->
+           second_order_matching_with_args ts env evd ev1 l1 (applist appr2))]
   | _,Evar ev2 when List.length l2 <= List.length l1 ->
       (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *)
-      first_order_unification ts env evd (ev2,l2) appr1
+      (* and otherwise second-order matching *)
+      ise_try evd
+        [(fun evd -> first_order_unification ts env evd (ev2,l2) appr1);
+         (fun evd ->
+           second_order_matching_with_args ts env evd ev2 l2 (applist appr1))]
   | Evar ev1,_ ->
       (* Try second-order pattern-matching *)
-      let evd,ev1 = evar_absorb_arguments env evd ev1 l1 in
-      second_order_matching ts env evd ev1 (applist appr2)
+      second_order_matching_with_args ts env evd ev1 l1 (applist appr2)
   | _,Evar ev2 ->
       (* Try second-order pattern-matching *)
-      let evd,ev2 = evar_absorb_arguments env evd ev2 l2 in
-      second_order_matching ts env evd ev2 (applist appr1)
+      second_order_matching_with_args ts env evd ev2 l2 (applist appr1)
   | _ ->
       (* Some head evar have been instantiated, or unknown kind of problem *)
       evar_conv_x ts env evd pbty t1 t2
-- 
cgit v1.2.3