diff options
| author | Hugo Herbelin | 2020-05-02 15:28:12 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-07 11:26:41 +0200 |
| commit | aa23fb72480182eddb7320ed59bf97448be7e04a (patch) | |
| tree | 54bdd9a58c834002675533de5dedd974dba230ee /engine/termops.mli | |
| parent | 325a644b3f5a5f8c1a86191004576e7c763ae9f3 (diff) | |
Termops: Adding functions local_occur_var_in_decl and occur_var_indirectly.
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index 4e77aa9b3b..709fa361a9 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -92,12 +92,14 @@ val occur_meta_or_existential : Evd.evar_map -> constr -> bool 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 (** As {!occur_var} but assume the identifier not to be a section variable *) val local_occur_var : Evd.evar_map -> Id.t -> constr -> bool +val local_occur_var_in_decl : Evd.evar_map -> Id.t -> named_declaration -> bool val free_rels : Evd.evar_map -> constr -> Int.Set.t |