From 2833dc95391a2eaf2c48cb7febac6eec8f07bfa4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 5 Mar 2011 16:42:30 +0000
Subject: Added support for instantiation of ?n by a lambda when "?n a" has to
 be unified with a (truly) rigid term.

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

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3906f87288..8b7fde3c29 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -374,7 +374,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
         let appr2 = evar_apprec env' evd [] c'2 in
 	evar_eqappr_x ts env' evd CONV appr1 appr2
 
-    | Flexible ev1, (Rigid _ | PseudoRigid _) ->
+    | Flexible ev1, (Rigid _ | PseudoRigid _ as c2) ->
 	if
 	  is_unification_pattern_evar env ev1 l1 (applist appr2) &
 	  not (occur_evar (fst ev1) (applist appr2))
@@ -385,12 +385,16 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  let t2 = solve_pattern_eqn env l1 t2 in
 	  solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem true pbty,ev1,t2)
+	else if is_rigid c2 & l1 <> [] then
+	  let (evd',c1) = define_evar_as_lambda env evd ev1 in
+	  evar_eqappr_x ts env evd' pbty
+	    (decompose_app (beta_applist (c1,l1))) appr2
 	else
 	  (* Postpone the use of an heuristic *)
 	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
 	  true
 
-    | (Rigid _ | PseudoRigid _), Flexible ev2 ->
+    | (Rigid _ | PseudoRigid _ as c1), Flexible ev2 ->
 	if
 	  is_unification_pattern_evar env ev2 l2 (applist appr1) &
 	  not (occur_evar (fst ev2) (applist appr1))
@@ -401,6 +405,10 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  let t1 = solve_pattern_eqn env l2 t1 in
 	  solve_simple_eqn (evar_conv_x ts) env evd
 	    (position_problem false pbty,ev2,t1)
+	else if is_rigid c1 & l2 <> [] then
+	  let (evd',c2) = define_evar_as_lambda env evd ev2 in
+	  evar_eqappr_x ts env evd' pbty appr1
+	    (decompose_app (beta_applist (c2,l2)))
 	else
 	  (* Postpone the use of an heuristic *)
 	  add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
-- 
cgit v1.2.3