diff options
| author | Maxime Dénès | 2017-11-06 17:15:35 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-06 17:18:44 +0100 |
| commit | c2a42557d0cc7c4c776a4572dcfeef011bfc73b8 (patch) | |
| tree | 9435d7ddc76abb74b7df0eec7abf861048dc89a2 /mathcomp/ssreflect/plugin | |
| parent | 7110a6e302fe102b6fb8df675511a44d8441d6c5 (diff) | |
Fix the only remaining spurious injection in the entire codebase.
We may want to make it an error, now that the transition period has been
long enough.
Diffstat (limited to 'mathcomp/ssreflect/plugin')
0 files changed, 0 insertions, 0 deletions