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, 1 insertions, 1 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 94b7ca96a..07a4dc8e2 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -259,7 +259,7 @@ val lookup_named_val : variable -> named_context_val -> named_declaration
(* XXX Missing Sigma proxy *)
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
+ Evd.evar_map -> Globnames.global_reference -> Evd.evar_map * t
val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool