diff options
| author | Vincent Laporte | 2019-03-14 17:17:38 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-14 17:17:38 +0000 |
| commit | 710a7cad94dcc9c734ab9ccc425f7a080dddc5f8 (patch) | |
| tree | a98a67f87b7bb2fee9b7f788a71672243825ab05 /kernel/nativecode.mli | |
| parent | 98914efd4193160d843092461674d6482aeee32e (diff) | |
| parent | 8ea0039ff69491b9e672bc3c522a356085d89c22 (diff) | |
Merge PR #9771: Exposes Coq_micromega.dump_proof_term to allow a use independent from tactics
Reviewed-by: vbgl
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions