diff options
Diffstat (limited to 'pretyping/indrec.ml')
-rw-r--r-- | pretyping/indrec.ml | 25 |
1 files changed, 4 insertions, 21 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 45eaae124..39aeb41f7 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -43,6 +43,7 @@ exception RecursionSchemeError of recursion_scheme_error let make_prod_dep dep env = if dep then mkProd_name env else mkProd let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c) + (*******************************************) (* Building curryfied elimination *) (*******************************************) @@ -376,27 +377,9 @@ let mis_make_indrec env sigma listdepkind mib u = (Anonymous,depind',concl)) arsign' in - let obj = - let projs = get_projections env indf in - match projs with - | None -> (mkCase (ci, pred, - mkRel 1, - branches)) - | Some ps -> - let branch = branches.(0) in - let ctx, br = decompose_lam_assum branch in - let n, subst = - List.fold_right (fun decl (i, subst) -> - match decl with - | LocalAssum (na,t) -> - let t = mkProj (Projection.make ps.(i) true, mkRel 1) in - i + 1, t :: subst - | LocalDef (na,b,t) -> - i, mkRel 0 :: subst) - ctx (0, []) - in - let term = substl subst br in - term + let obj = + Inductiveops.make_case_or_project env indf ci pred + (mkRel 1) branches in it_mkLambda_or_LetIn_name env obj (Termops.lift_rel_context nrec deparsign) |