diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-05-25 15:17:28 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-07-06 14:38:05 +0200 |
| commit | f8a5cb590352a617de38fdd8ba5ffff7691d9841 (patch) | |
| tree | 5a4414e9e6d41fe0ebcccf5b25770b20bc31469d /pretyping/indrec.ml | |
| parent | f77c2b488ca552b2316d4ebab1c051cb5a1347ab (diff) | |
Disallow dependent case on prim records w/o eta
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) |