diff options
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index d25f8a837..7bd616591 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -122,11 +122,16 @@ val inductive_has_local_defs : inductive -> bool val allowed_sorts : env -> inductive -> sorts_family list +(** (Co)Inductive records with primitive projections do not have eta-conversion, + hence no dependent elimination. *) +val has_dependent_elim : mutual_inductive_body -> bool + (** Primitive projections *) val projection_nparams : projection -> int val projection_nparams_env : env -> projection -> int val type_of_projection_knowing_arg : env -> evar_map -> Projection.t -> - constr -> types -> types + constr -> types -> types + (** Extract information from an inductive family *) @@ -175,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*) |