summaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/inductive.ml')
-rw-r--r--kernel/inductive.ml9
1 files changed, 1 insertions, 8 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index bb57ad25..ca814f49 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -364,7 +364,7 @@ let build_branches_type (ind,u) (_,mip as specif) params p =
let cstr = ith_constructor_of_inductive ind (i+1) in
let dep_cstr = applist (mkConstructU (cstr,u),lparams@(local_rels args)) in
vargs @ [dep_cstr] in
- let base = beta_appvect (lift nargs p) (Array.of_list cargs) in
+ let base = betazeta_appvect mip.mind_nrealdecls (lift nargs p) (Array.of_list cargs) in
it_mkProd_or_LetIn base args in
Array.mapi build_one_branch mip.mind_nf_lc
@@ -447,13 +447,6 @@ type subterm_spec =
let eq_wf_paths = Rtree.equal Declareops.eq_recarg
-let pp_recarg = function
- | Norec -> Pp.str "Norec"
- | Mrec i -> Pp.str ("Mrec "^MutInd.to_string (fst i))
- | Imbr i -> Pp.str ("Imbr "^MutInd.to_string (fst i))
-
-let pp_wf_paths = Rtree.pp_tree pp_recarg
-
let inter_recarg r1 r2 = match r1, r2 with
| Norec, Norec -> Some r1
| Mrec i1, Mrec i2