diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-06-04 12:23:14 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:23:14 +0200 |
| commit | 86535d84cc3cffeee1dcd8545343f234e7285530 (patch) | |
| tree | 9b221c283c2971f7ac151397231059e1d239e723 /pretyping/vnorm.ml | |
| parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) | |
| parent | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff) | |
Remove non-DFSG contentsupstream/8.4_gamma0+really8.4beta2+dfsg
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index fad2e6f0..ac3df714 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -109,7 +109,7 @@ let build_branches_type env (mind,_ as _ind) mib mip params dep p = a 0) et les lambda correspondant aux realargs *) let build_one_branch i cty = let typi = type_constructor mind mib cty params in - let decl,indapp = Term.decompose_prod typi in + let decl,indapp = decompose_prod_assum typi in let ind,cargs = find_rectype_a env indapp in let nparams = Array.length params in let carity = snd (rtbl.(i)) in @@ -193,11 +193,8 @@ and nf_stk env c t stk = let bsw = branch_of_switch (nb_rel env) sw in let mkbranch i (n,v) = let decl,codom = btypes.(i) in - let env = - List.fold_right - (fun (name,t) env -> push_rel (name,None,t) env) decl env in - let b = nf_val env v codom in - compose_lam decl b + let b = nf_val (push_rel_context decl env) v codom in + it_mkLambda_or_LetIn b decl in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type dep p realargs c in |