diff options
| author | Paul Steckler | 2017-08-16 15:06:43 -0400 |
|---|---|---|
| committer | Paul Steckler | 2017-08-16 15:06:43 -0400 |
| commit | 7f3a7aa17cddfda15146117f7f8a6c40a91ab243 (patch) | |
| tree | d7e903cf7edfb9b24728da3002d759e538bb3d70 /kernel/nativelib.ml | |
| parent | 8c2799476f669e82ea0d49adb2a2dcec6c05e35b (diff) | |
mention that tactic is the identity or gives error
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions