From dfd0b49514120f90ce558cf8b017e2e7c993ef95 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Fri, 11 May 2012 20:24:06 +0000
Subject: Impossible branches inference fixup (bug 2761)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15307 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ef3408414c..6a9b074105 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1480,7 +1480,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 			  [dummy_loc,[],thepats, (* "|p1,..,pn" *)
 			   Option.cata (intern_type env') (GHole(dummy_loc,Evd.CasesType)) rtnpo; (* "=> P" is there were a P "=> _" else *)
 			   dummy_loc,[],list_make (List.length thepats) (PatVar(dummy_loc,Anonymous)), (* "|_,..,_" *)
-			   GHole(dummy_loc,Evd.CasesType) (* "=> _" *)]))
+			   GHole(dummy_loc,Evd.ImpossibleCase) (* "=> _" *)]))
 	in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
 	GCases (loc, sty, rtnpo, tms, List.flatten eqns')
-- 
cgit v1.2.3