diff options
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 |