diff options
| author | Pierre-Marie Pédrot | 2016-05-02 11:34:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-02 11:34:40 +0200 |
| commit | 35d6aa4bc7c2d39bbd55d2ff5d114a03e1f284f2 (patch) | |
| tree | 613f0924d8e1004174a7658c3fd414ecf8afdb69 /mathcomp/field | |
| parent | 374222f28aea5f8cdce246fb9e7b68b612a4349e (diff) | |
Fixing compilation after the merge of ML-tactic-notation branch.
Diffstat (limited to 'mathcomp/field')
0 files changed, 0 insertions, 0 deletions