diff options
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 19613c4e..8198db1b 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -166,8 +166,15 @@ and nf_whd env whd typ = 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 - let args = nf_bargs env b ctyp in + 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 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 |