diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-12-02 17:46:03 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-12-02 17:46:03 +0100 |
| commit | 9dfbf93bf1d587d330b62b4f551c499f18a470e9 (patch) | |
| tree | cc9d38ad3ef1c153be0dfb800f47320a7e586bef /pretyping/glob_ops.ml | |
| parent | e83ffcd53acdebfbbd927b3c9b48a0d1ad6ca9e5 (diff) | |
| parent | 27190db7f119bc9b50150be6dff889986c747e38 (diff) | |
Merge remote-tracking branch 'github/pr/368' into v8.6
Was PR#368: Add example in dev/doc/changes involving Tacmach.project
Diffstat (limited to 'pretyping/glob_ops.ml')
0 files changed, 0 insertions, 0 deletions