diff options
| author | Kazuhiko Sakaguchi | 2020-06-16 02:09:36 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-06-27 13:06:00 +0900 |
| commit | 4a0bc9e3de7a19439f45ba59405015033607ed68 (patch) | |
| tree | b587d94bfe8edc93be5bbb76caba767d4e0ff3d2 /mathcomp/Makefile.common | |
| parent | 3728862662bd0a5b836dfa746921954604d051ec (diff) | |
Fix bugs in hierarchy.ml
- pass `Unix.environment ()` to `coqtop` to preserve the parent process
environment,
- check the exit status of `coqtop` and report an error if it is wrong,
- do not rely on `ssrfun.id` in the `check_join` tactic, and
- improve the error message for missing unification hints.
Diffstat (limited to 'mathcomp/Makefile.common')
0 files changed, 0 insertions, 0 deletions