diff options
| author | Enrico Tassi | 2020-08-13 18:18:20 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2020-08-13 18:18:20 +0200 |
| commit | ca47fb67a95cf291a43a68b210b9670d4461e9d6 (patch) | |
| tree | 509fbb6f8643496489ce798b8ce05706520b5623 /pretyping/reductionops.mli | |
| parent | 422e2ec9cc902bfb3f6ea78045e8490328acbd20 (diff) | |
| parent | 0c576f95fe6a804babd0ff2f296b3f112eda8ff9 (diff) | |
Merge PR #12823: Move reduce_mind_case from Reductionops to Tacred.
Reviewed-by: gares
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 0f288cdd46..d404a7e414 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -217,22 +217,14 @@ val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr (** Raises [Invalid_argument] *) - -type 'a miota_args = { - mP : constr; (** the result type *) - mconstr : constr; (** the constructor *) - mci : case_info; (** special info to re-build pattern *) - mcargs : 'a list; (** the constructor's arguments *) - mlf : 'a array } (** the branch code vector *) - val reducible_mind_case : evar_map -> constr -> bool -val reduce_mind_case : evar_map -> constr miota_args -> constr val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, EInstance.t) kind_of_term val is_arity : env -> evar_map -> constr -> bool val is_sort : env -> evar_map -> types -> bool val contract_fix : evar_map -> fixpoint -> constr +val contract_cofix : evar_map -> cofixpoint -> constr (** {6 Querying the kernel conversion oracle: opaque/transparent constants } *) val is_transparent : Environ.env -> Constant.t tableKey -> bool |