diff options
| author | Matthieu Sozeau | 2016-05-25 13:49:50 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-07-06 14:38:05 +0200 |
| commit | f77c2b488ca552b2316d4ebab1c051cb5a1347ab (patch) | |
| tree | 1efb41cfb54c9b06b70971b788e928e430c7e58c /pretyping/inductiveops.mli | |
| parent | a7ed091b6842cc78f0480504e84c3cfa261860bd (diff) | |
Renaming to more generic has_dependent_elim test
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 6c49099a8f..7ef848f0de 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -122,14 +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 -(** Recursive records with primitive projections do not have eta-conversion *) -val is_primitive_record_without_eta : mutual_inductive_body -> bool (** Extract information from an inductive family *) |