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/inductiveops.mli | |
| parent | f77c2b488ca552b2316d4ebab1c051cb5a1347ab (diff) | |
Disallow dependent case on prim records w/o eta
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 7ef848f0d..7bd616591 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -180,6 +180,14 @@ val type_case_branches_with_names : (** Annotation for cases *) val make_case_info : env -> inductive -> case_style -> case_info +(** Make a case or substitute projections if the inductive type is a record + with primitive projections. + Fail with an error if the elimination is dependent while the + inductive type does not allow dependent elimination. *) +val make_case_or_project : + env -> inductive_family -> case_info -> + (* pred *) constr -> (* term *) constr -> (* branches *) constr array -> constr + (*i Compatibility val make_default_case_info : env -> case_style -> inductive -> case_info i*) |