diff options
| author | Hugo Herbelin | 2017-04-30 23:35:35 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-31 00:46:01 +0200 |
| commit | 679d8ba37c05a43b0480a4200bfb1347481a5d1a (patch) | |
| tree | 7fc5a30d3a38f98d1b6c51d1d75fb7bb99d6fb7b /mathcomp/Make | |
| parent | c05bfbee9a753b8867bc6ea5847cb7dd696a0cbd (diff) | |
Binding glob_constr to interp_glob_closure so as to factorize low-level code.
Diffstat (limited to 'mathcomp/Make')
0 files changed, 0 insertions, 0 deletions