diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-22 21:33:15 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-22 21:33:15 +0000 |
| commit | daae294d35dd3ea8655a989681944654087dbf97 (patch) | |
| tree | d4d03851cda2c885e2b8801ee83ca71dc068db19 /pretyping | |
| parent | 2730a0214dd2f73a286cf92215ccc0d54278f544 (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 283363f37..f39942025 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 |