diff options
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 54e88f646..d378501a0 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -165,7 +165,7 @@ val set_engagement : engagement -> env -> env val global_vars_set : env -> constr -> Id.Set.t (** the constr must be a global reference *) -val vars_of_global : env -> constr -> Id.t list +val vars_of_global : env -> constr -> Id.Set.t val keep_hyps : env -> Id.Set.t -> section_context |