aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--pretyping/termops.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 317a375632..ca5e5139df 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -185,3 +185,4 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr
(* Test if an identifier is the basename of a global reference *)
val is_global : identifier -> bool
+val is_section_variable : identifier -> bool