From 924a6e99f85aa0d70d42e753d6901b067ebf8f1d Mon Sep 17 00:00:00 2001
From: Benjamin Gregoire
Date: Fri, 27 Mar 2015 06:44:02 +0100
Subject: use a more compact representation of non-constant constructors for
 which there corresponding tag are greater than max_variant_tag. The code is a
 merge with the patch proposed by Bruno on github barras/coq
 commit/504c753d7bb104ff4453fa0ede21c870ae2bb00c

---
 pretyping/vnorm.ml | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 3c302f8da3..8198db1b8a 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -165,9 +165,16 @@ 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 (tag,b) ->
+  | Vconstr_block b ->
+      let tag = btag b in
+      let (tag,ofs) =
+        if tag = Cbytecodes.last_variant_tag then
+	  match whd_val (bfield b 0) with
+	  | Vconstr_const tag -> (tag+Cbytecodes.last_variant_tag, 1)
+	  | _ -> assert false
+        else (tag, 0) in
       let capp,ctyp = construct_of_constr_block env tag typ in
-      let args = nf_bargs env b ctyp in
+      let args = nf_bargs env b ofs ctyp in
       mkApp(capp,args)
   | Vatom_stk(Aid idkey, stk) ->
       let c,typ = constr_type_of_idkey env idkey in
@@ -242,14 +249,14 @@ and nf_args env vargs t =
 	t := subst1 c codom; c) in
   !t,args
 
-and nf_bargs env b t =
+and nf_bargs env b ofs t =
   let t = ref t in
-  let len = bsize b in
+  let len = bsize b - ofs in
   let args =
     Array.init len
       (fun i ->
 	let _,dom,codom = decompose_prod env !t in
-	let c = nf_val env (bfield b i) dom in
+	let c = nf_val env (bfield b (i+ofs)) dom in
 	t := subst1 c codom; c) in
   args
 
-- 
cgit v1.2.3