From aadd90837e8e0eb015e4e4999394ca56f55f70b8 Mon Sep 17 00:00:00 2001
From: bgregoir
Date: Fri, 25 Nov 2011 12:34:26 +0000
Subject: avoid relying on weak invariant in cbv.ml

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

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index cd83145734..ad33bae1fb 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -290,7 +290,7 @@ and cbv_stack_term info stack env t =
         cbv_stack_term info (stack_app cargs stk) env br.(n-1)
 
     (* constructor of arity 0 in a Case -> IOTA *)
-    | (CONSTR((_,n),_), CASE(_,br,_,env,stk))
+    | (CONSTR((_,n),[||]), CASE(_,br,_,env,stk))
             when red_set (info_flags info) fIOTA ->
                     cbv_stack_term info stk env br.(n-1)
 
-- 
cgit v1.2.3