diff options
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index b0d714b03..506cdd8c9 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -194,6 +194,10 @@ val make_case_or_project : val make_default_case_info : env -> case_style -> inductive -> case_info i*) +val compute_projections : Environ.env -> inductive -> (constr * types) array +(** Given a primitive record type, for every field computes the eta-expanded + projection and its type. *) + (********************) val type_of_inductive_knowing_conclusion : |