diff options
| author | Enrico | 2016-05-04 14:15:00 +0200 |
|---|---|---|
| committer | Enrico | 2016-05-04 14:15:00 +0200 |
| commit | 0fedd37679abe2a9909ec03aebf01aab359a06fd (patch) | |
| tree | 613f0924d8e1004174a7658c3fd414ecf8afdb69 /mathcomp/character/mxrepresentation.v | |
| parent | 374222f28aea5f8cdce246fb9e7b68b612a4349e (diff) | |
| parent | 35d6aa4bc7c2d39bbd55d2ff5d114a03e1f284f2 (diff) | |
Merge pull request #40 from ppedrot/partial-fix
Fixing compilation after the merge of ML-tactic-notation branch.
Diffstat (limited to 'mathcomp/character/mxrepresentation.v')
0 files changed, 0 insertions, 0 deletions