diff options
| author | Pierre-Marie Pédrot | 2018-04-10 18:24:45 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-04-10 19:15:42 +0200 |
| commit | 7913b03ba5072efeb9f6ef009ce27cec8ff19cac (patch) | |
| tree | bd6b9cdf466c6a4c7973b2209d0c292e05bd854d /engine/termops.mli | |
| parent | 834530272b9006e28a4b7ba35b1f8f861f51e7ce (diff) | |
Replace uses of Termops.dependent by more specific functions.
This is more efficient in general, because Termops.dependent doesn't take
advantage of the knowledge of its pattern argument.
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index 3b0c4bba64..54b47f9e4a 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -94,6 +94,7 @@ exception Occur val occur_meta : Evd.evar_map -> constr -> bool val occur_existential : Evd.evar_map -> constr -> bool 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_in_decl : |