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 /_CoqProject | |
| 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 '_CoqProject')
0 files changed, 0 insertions, 0 deletions