diff options
| author | Maxime Dénès | 2014-10-21 13:57:59 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2014-10-21 13:57:59 +0200 |
| commit | 0c397c1004b099f2cb1104e8fb9e5c1e10b5ba54 (patch) | |
| tree | 9a49379b729d1aaeeac62799019b5048ff79ad0e | |
| parent | 9aa960939cb02e655b40d67f42a3df2bcf3f73c3 (diff) | |
Porting Hugo's fix 98f3abb83a to native compiler.
| -rw-r--r-- | pretyping/nativenorm.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 60db95e25f..9f1a19da1f 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -101,7 +101,8 @@ 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 = Reductionops.splay_prod env Evd.empty typi in + let decl_with_letin,_ = 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 @@ -115,7 +116,7 @@ let build_branches_type env (mind,_ as _ind) mib mip params dep p = mkApp(papp,[|dep_cstr|]) else papp in - decl, codom + decl, decl_with_letin, codom in Array.mapi build_one_branch mip.mind_nf_lc let build_case_type dep p realargs c = @@ -300,12 +301,9 @@ and nf_atom_type env atom = (* calcul des branches *) let bsw = branch_of_switch (nb_rel env) ans bs in let mkbranch i 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 decl,decl_with_letin,codom = btypes.(i) in + let b = nf_val (Termops.push_rels_assum decl env) v codom in + Termops.it_mkLambda_or_LetIn_from_no_LetIn b decl_with_letin in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type dep p realargs a in |