diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 10:21:17 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-16 10:37:53 +0200 |
| commit | 025c4f63b28671a24bd6c46f9b23a3dad76fd179 (patch) | |
| tree | 2759d9c0eaa5e62329727677bf54caf06ac9ffe6 /pretyping/evd.ml | |
| parent | e6708590ce648921f27395ce535e35d52aa2cc0f (diff) | |
Goal: remove [advance] from the API.
Now [Goal] only contains a few helpers.
Diffstat (limited to 'pretyping/evd.ml')
0 files changed, 0 insertions, 0 deletions