diff options
| author | Hugo Herbelin | 2020-03-15 11:11:19 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-07-17 18:07:21 +0200 |
| commit | a34ba68fd83f6044da3255c4a0f91c141aafceda (patch) | |
| tree | cef39208a9f2a0d3d95c4821219a2b34518db808 /dev/include_dune | |
| parent | e221ebd6c8b485274b809768c965f2653094fd8f (diff) | |
Documenting new primitive entry evaluable_ref usable for tactic notations.
Diffstat (limited to 'dev/include_dune')
0 files changed, 0 insertions, 0 deletions