diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 10:36:12 +0200 |
commit | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (patch) | |
tree | 12e8931a4a56da1a1bdfb89d670f4ba38fe08e1f /pretyping/vnorm.ml | |
parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) |
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
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 |