aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/eConstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/eConstr.mli')
-rw-r--r--engine/eConstr.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 06020c573..94b7ca96a 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -261,6 +261,8 @@ val fresh_global :
?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
'r Sigma.t -> Globnames.global_reference -> (t, 'r) Sigma.sigma
+val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool
+
(** {5 Extra} *)
val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt