diff options
Diffstat (limited to 'kernel/declareops.mli')
| -rw-r--r-- | kernel/declareops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 23a44433b3..54a853fc81 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -70,6 +70,8 @@ val inductive_make_projection : Names.inductive -> mutual_inductive_body -> proj val inductive_make_projections : Names.inductive -> mutual_inductive_body -> Names.Projection.Repr.t array option +val relevance_of_projection_repr : mutual_inductive_body -> Names.Projection.Repr.t -> Sorts.relevance + (** {6 Kernel flags} *) (** A default, safe set of flags for kernel type-checking *) |