aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/attic/tutorial.v
diff options
context:
space:
mode:
authorMaxime Dénès2017-11-06 17:15:35 +0100
committerMaxime Dénès2017-11-06 17:18:44 +0100
commitc2a42557d0cc7c4c776a4572dcfeef011bfc73b8 (patch)
tree9435d7ddc76abb74b7df0eec7abf861048dc89a2 /mathcomp/attic/tutorial.v
parent7110a6e302fe102b6fb8df675511a44d8441d6c5 (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/attic/tutorial.v')
0 files changed, 0 insertions, 0 deletions