aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/eConstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/eConstr.ml')
-rw-r--r--engine/eConstr.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index c0485e4e7..5a05150d4 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -782,6 +782,9 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
Sigma.fresh_global ?loc ?rigid ?names env sigma reference in
Sigma.Sigma (of_constr t,sigma,p)
+let is_global sigma gr c =
+ Globnames.is_global gr (to_constr sigma c)
+
module Unsafe =
struct
let to_sorts = ESorts.unsafe_to_sorts