diff options
| author | Gaëtan Gilbert | 2021-02-17 13:56:27 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-02-17 13:56:27 +0100 |
| commit | 441bace297a4c31e5003cec93e46e6a47fa684d3 (patch) | |
| tree | 61bbdab449271979489b3ad9bba61faae751aa34 /pretyping/inductiveops.mli | |
| parent | a192260d8be92e2435445dcdd0484577c7fd6671 (diff) | |
Use make_case_or_project in auto_ind_decl
Towards #5154 (but insufficient)
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 8e83814fa0..59ef8e08e3 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -212,6 +212,12 @@ val make_case_or_project : env -> evar_map -> inductive_type -> case_info -> (* pred *) EConstr.constr -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr +(** Sometimes [make_case_or_project] is nicer to call with a pre-built + [case_invert] than [inductive_type]. *) +val simple_make_case_or_project : + env -> evar_map -> case_info -> + (* pred *) EConstr.constr -> EConstr.case_invert -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr + val make_case_invert : env -> inductive_type -> case_info -> EConstr.case_invert |