diff options
| author | Gaëtan Gilbert | 2017-10-31 17:04:02 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 13:27:38 +0100 |
| commit | 23f84f37c674a07e925925b7e0d50d7ee8414093 (patch) | |
| tree | 7e470de5769c994d8df37c44fed12cf299d5b194 /pretyping/retyping.mli | |
| parent | 75508769762372043387c67a9abe94e8f940e80a (diff) | |
Add relevance marks on binders.
Kernel should be mostly correct, higher levels do random stuff at
times.
Diffstat (limited to 'pretyping/retyping.mli')
| -rw-r--r-- | pretyping/retyping.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 2aff0c7775..252bfb1a84 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -53,3 +53,8 @@ val sorts_of_context : env -> evar_map -> rel_context -> Sorts.t list val expand_projection : env -> evar_map -> Names.Projection.t -> constr -> constr list -> constr val print_retype_error : retype_error -> Pp.t + +val relevance_of_term : env -> evar_map -> constr -> Sorts.relevance +val relevance_of_type : env -> evar_map -> types -> Sorts.relevance +val relevance_of_sort : ESorts.t -> Sorts.relevance +val relevance_of_sort_family : Sorts.family -> Sorts.relevance |