diff options
| author | coqbot-app[bot] | 2020-09-25 15:06:01 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-25 15:06:01 +0000 |
| commit | 9c2228ff011dc6188b70084fa1e1a5158affcf24 (patch) | |
| tree | 3ba7d6864516fe66ec17904d78cf1905c251d960 /pretyping/pretype_errors.mli | |
| parent | 39fe24769d18c21379f1123754fd606cdf8cd4c8 (diff) | |
| parent | fc0aa1e70cb1891ef3f62566af4e551d06bfb613 (diff) | |
Merge PR #12999: More improvements in locating tactic errors
Reviewed-by: ppedrot
Reviewed-by: ejgallego
Diffstat (limited to 'pretyping/pretype_errors.mli')
0 files changed, 0 insertions, 0 deletions