aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/vconv.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/vconv.ml')
-rw-r--r--kernel/vconv.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 5ef84adc7..cdc9fa0f7 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -318,7 +318,7 @@ let find_rectype typ =
let construct_of_constr_block env tag typ =
let (mind,_ as ind),allargs = find_rectype (whd_betadeltaiota env typ) in
let (mib,mip) = Inductive.lookup_mind_specif env ind in
- let nparams = mip.mind_nparams in
+ let nparams = mib.mind_nparams in
let rtbl = mip.mind_reloc_tbl in
let i = invert_tag false tag rtbl in
let params = Array.sub allargs 0 nparams in
@@ -429,7 +429,7 @@ and nf_stk env c t stk =
| Zswitch sw :: stk ->
let (mind,_ as ind),allargs = find_rectype (whd_betadeltaiota env t) in
let (mib,mip) = Inductive.lookup_mind_specif env ind in
- let nparams = mip.mind_nparams in
+ let nparams = mib.mind_nparams in
let params,realargs = Util.array_chop nparams allargs in
(* calcul du predicat du case,
[dep] indique si c'est un case dependant *)