diff options
| author | Emilio Jesus Gallego Arias | 2019-07-17 16:33:41 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-31 11:13:04 +0200 |
| commit | fac3d5e2159ddafb947448ee42aa892325f320ee (patch) | |
| tree | a8737f5227bf2836107dfece63aef8b1c004c950 /kernel/nativecode.mli | |
| parent | ce22c1cb3bca8381d9b0ebfef2fbf27e92418b0c (diff) | |
[funind] Move duplicated `observe_tac` function to indfun_common.
We also attempt a version that may work with `Proofview.tactic` , may
need more work.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions