aboutsummaryrefslogtreecommitdiff
path: root/engine/termops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/termops.mli')
-rw-r--r--engine/termops.mli6
1 files changed, 3 insertions, 3 deletions
diff --git a/engine/termops.mli b/engine/termops.mli
index bdde2c450d..0faebecb1b 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -89,9 +89,9 @@ val occur_metavariable : Evd.evar_map -> metavariable -> constr -> bool
val occur_evar : Evd.evar_map -> Evar.t -> constr -> bool
val occur_var : env -> Evd.evar_map -> Id.t -> constr -> bool
val occur_var_indirectly : env -> Evd.evar_map -> Id.t -> constr -> GlobRef.t option
-val occur_var_in_decl :
- env -> Evd.evar_map ->
- Id.t -> named_declaration -> bool
+val occur_var_in_decl : env -> Evd.evar_map -> Id.t -> named_declaration -> bool
+val occur_vars : env -> Evd.evar_map -> Id.Set.t -> constr -> bool
+val occur_vars_in_decl : env -> Evd.evar_map -> Id.Set.t -> named_declaration -> bool
(** As {!occur_var} but assume the identifier not to be a section variable *)
val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool