diff options
| author | Pierre-Marie Pédrot | 2016-05-13 17:19:08 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-18 11:46:43 +0200 |
| commit | 1327aada8c68d8ba5ff97b22f4296a3cd5a33f6e (patch) | |
| tree | 0eff554ade7ed76339b532954674bf4766fdd8e6 /mathcomp/Make | |
| parent | d9cecc8f2f1d38947e4889b996c42b26c08f9be1 (diff) | |
Fix compilation after the change of API in Tactics.
Diffstat (limited to 'mathcomp/Make')
0 files changed, 0 insertions, 0 deletions