diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index c9cafccec4..6e6c243c76 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -104,6 +104,7 @@ val is_info_arity : 'c unsafe_env -> constr -> bool val is_info_sort : 'c unsafe_env -> constr -> bool val is_logic_arity : 'c unsafe_env -> constr -> bool val is_type_arity : 'c unsafe_env -> constr -> bool +val is_info_type : 'c unsafe_env -> typed_type -> bool val is_info_cast_type : 'c unsafe_env -> constr -> bool val contents_of_cast_type : 'c unsafe_env -> constr -> contents val poly_args : 'a unsafe_env -> constr -> int list |