diff options
| author |  Jason Gross <jasongross9@gmail.com> | 2016-11-21 15:05:26 -0500 |
|---|---|---|
| committer |  GitHub <noreply@github.com> | 2016-11-21 15:05:26 -0500 |
| commit | 27190db7f119bc9b50150be6dff889986c747e38 (patch) | |
| tree | 959f62953bf9d2928489aa53bf67e6288621a172 /pretyping/glob_ops.ml | |
| parent | aa86963464045d61fa0eaf3a7fe67ced7a6a73f4 (diff) | |
(v8.6) Add example in dev/doc/changes involving Tacmach.project
Diffstat (limited to 'pretyping/glob_ops.ml')
0 files changed, 0 insertions, 0 deletions