aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/Make
diff options
context:
space:
mode:
authorMaxime Dénès2017-06-06 09:09:24 +0200
committerGitHub2017-06-06 09:09:24 +0200
commitc8d04cb7e9fa6c6717ae8021d0ce86b9c134cbe6 (patch)
treec4b047a1f072d8e53dd4a9e6fd312f2b3a973646 /mathcomp/Make
parent329fa19cc1d35162ce7c8ef82e3bf36aec058b26 (diff)
parent679d8ba37c05a43b0480a4200bfb1347481a5d1a (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 'mathcomp/Make')
0 files changed, 0 insertions, 0 deletions