diff options
| author | Emilio Jesus Gallego Arias | 2019-04-30 23:58:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-30 23:58:26 +0200 |
| commit | d6ebee1ad4b56d769227fab7373667eda3352fec (patch) | |
| tree | a3d17a4a72ff4d07e4df0301e43969d5895c2018 /doc/plugin_tutorial/tuto1/src/simple_declare.ml | |
| parent | 0ad2733e202f98953c6bc1569d191a36b746df03 (diff) | |
| parent | 77257819ea4a381067e65fd46e7d7590aa7e2600 (diff) | |
Merge PR #9947: Remove Global.env from goptions by passing from vernacentries
Reviewed-by: ejgallego
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_declare.ml')
0 files changed, 0 insertions, 0 deletions