diff options
| author | coqbot-app[bot] | 2021-04-25 18:02:47 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-25 18:02:47 +0000 |
| commit | 6683de2eaa499bd269e75d064a1674d5e4d10d34 (patch) | |
| tree | 18c03d4b603a74b20a2935c4a12ed72d505f44a1 /engine/termops.mli | |
| parent | d9e9a63f9f49768eee8b239812365ad1115b964f (diff) | |
| parent | 9caadc38de0e1c7b3362081da9482fc4455220a7 (diff) | |
Reviewed-by: herbelin
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 6 |
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 |