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 /kernel/type_errors.mli | |
| parent | 325a644b3f5a5f8c1a86191004576e7c763ae9f3 (diff) | |
Termops: Adding functions local_occur_var_in_decl and occur_var_indirectly.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions