From 5c6a50d6ec1d04bacd3e41ffbb88453fef92cd5d Mon Sep 17 00:00:00 2001
From: Benjamin Gregoire
Date: Thu, 26 Mar 2015 14:24:54 +0100
Subject: Fix bug 4157, change the representation of inductive constructor when
 there is too many non constant constructors in the inductive type Conflicts: 
 kernel/cbytegen.ml

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

(limited to 'pretyping')

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 19613c4e06..3c302f8da3 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -165,8 +165,8 @@ and nf_whd env whd typ =
       let _, args = nf_args env vargs t in
       mkApp(cfd,args)
   | Vconstr_const n -> construct_of_constr_const env n typ
-  | Vconstr_block b ->
-      let capp,ctyp = construct_of_constr_block env (btag b) typ in
+  | Vconstr_block (tag,b) ->
+      let capp,ctyp = construct_of_constr_block env tag typ in
       let args = nf_bargs env b ctyp in
       mkApp(capp,args)
   | Vatom_stk(Aid idkey, stk) ->
-- 
cgit v1.2.3