aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/declarations.mli
diff options
context:
space:
mode:
Diffstat (limited to 'checker/declarations.mli')
-rw-r--r--checker/declarations.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 456df8369..6fc71bb94 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -14,6 +14,7 @@ val body_of_constant : constant_body -> constr option
val constant_has_body : constant_body -> bool
val is_opaque : constant_body -> bool
val opaque_univ_context : constant_body -> Univ.ContextSet.t
+val constant_is_polymorphic : constant_body -> bool
(* Mutual inductives *)