diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/nativenorm.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index af7a99320b..b635229cfd 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -70,8 +70,15 @@ let type_constructor mind mib typ params = let construct_of_constr_notnative const env tag (mind, _ as ind) allargs = let mib,mip = lookup_mind_specif env ind in let nparams = mib.mind_nparams in - let i = invert_tag const tag mip.mind_reloc_tbl in let params = Array.sub allargs 0 nparams in + try + if const then + let ctyp = type_constructor mind mib (mip.mind_nf_lc.(0)) params in + retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd ind) tag, ctyp + else + raise Not_found + with Not_found -> + let i = invert_tag const tag mip.mind_reloc_tbl in let ctyp = type_constructor mind mib (mip.mind_nf_lc.(i-1)) params in (mkApp(mkConstruct(ind,i), params), ctyp) |