aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/termops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/termops.mli')
-rw-r--r--engine/termops.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/engine/termops.mli b/engine/termops.mli
index 02e8dfeae..abc9caa98 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -268,6 +268,8 @@ val is_section_variable : Id.t -> bool
val global_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference puniverses
+val is_global : Evd.evar_map -> Globnames.global_reference -> EConstr.constr -> bool
+
val isGlobalRef : Evd.evar_map -> EConstr.t -> bool
val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool