diff options
| author | coqbot-app[bot] | 2020-12-12 18:11:12 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-12 18:11:12 +0000 |
| commit | 81d0936c1ac8a537b5d8083933bce607e55ff28f (patch) | |
| tree | f796eff07f22c308502ad31373b079952a4aed60 /kernel/nativelib.mli | |
| parent | 233629e8f6e40057a8caf7502047995427740ae8 (diff) | |
| parent | 7615b53cbcee95677996d60eb1c5ecc667559759 (diff) | |
Merge PR #13620: Use a registered printer for tactic coercion failure.
Reviewed-by: ejgallego
Ack-by: herbelin
Diffstat (limited to 'kernel/nativelib.mli')
0 files changed, 0 insertions, 0 deletions