diff options
| author | Maxime Dénès | 2017-06-06 09:09:24 +0200 |
|---|---|---|
| committer | GitHub | 2017-06-06 09:09:24 +0200 |
| commit | c8d04cb7e9fa6c6717ae8021d0ce86b9c134cbe6 (patch) | |
| tree | c4b047a1f072d8e53dd4a9e6fd312f2b3a973646 /docs/htmldoc | |
| parent | 329fa19cc1d35162ce7c8ef82e3bf36aec058b26 (diff) | |
| parent | 679d8ba37c05a43b0480a4200bfb1347481a5d1a (diff) | |
Merge pull request #127 from herbelin/trunk+interp_closed_glob_constr
Binding glob_constr to interp_glob_closure so as to factorize low-level code.
Diffstat (limited to 'docs/htmldoc')
0 files changed, 0 insertions, 0 deletions