From 2ce9f694faf3ea69b0eeb0a5b4214852bcbffc58 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 2 Jul 2014 17:19:13 +0200
Subject: Fix a Not_found anomaly raised by solve_evar_evar, we were breaking
 the invariant that the evar arguments to that function always have to be
 undefined.

---
 pretyping/evarsolve.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 13421bcde4..d15c5d00bd 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1159,9 +1159,8 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar
 	      ?candidates:evi.evar_candidates (it_mkProd_or_LetIn (mkSort k) ctx) 
 	  in
 	  let evd = Evd.set_leq_sort (Evd.set_leq_sort evd k i) k j in
-	    solve_evar_evar ~force f g env 
-	      (solve_evar_evar ~force f g env evd None (ev3,args1) ev1)
-	      pbty (ev3,args1) ev2
+	  let evd = solve_evar_evar ~force f g env evd (Some false) (ev3,args1) ev1 in
+	    f env evd pbty ev2 (whd_evar evd (mkEvar (ev3,args1)))
     with Reduction.NotArity -> 
       solve_evar_evar ~force f g env evd None ev1 ev2
 
-- 
cgit v1.2.3