From da178a880e3ace820b41d38b191d3785b82991f5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 1 Jul 2010 17:21:14 +0200
Subject: Imported Upstream version 8.2pl2+dfsg

---
 proofs/logic.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs/logic.ml')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index caf6f56b..c019d45f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
+(* $Id: logic.ml 12240 2009-07-15 09:52:52Z herbelin $ *)
 
 open Pp
 open Util
@@ -438,7 +438,7 @@ and mk_casegoals sigma goal goalacc p c =
   let (acc'',pt) = mk_hdgoals sigma goal acc' p in
   let pj = {uj_val=p; uj_type=pt} in 
   let indspec =
-    try find_mrectype env sigma ct
+    try find_mrectype env sigma (nf_evar sigma ct)
     with Not_found -> anomaly "mk_casegoals" in
   let (lbrty,conclty) =
     type_case_branches_with_names env indspec pj c in
-- 
cgit v1.2.3