diff options
| author | Maxime Dénès | 2014-05-18 13:04:52 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-05-18 13:04:52 -0400 |
| commit | 076274d366f7dd4f09d99fa8f3962b6f78bf9252 (patch) | |
| tree | 75adc332d0ea1e7176ba2c9ac1c01fd64d33b9d4 /dev/base_include | |
| parent | e1cf5ccd8df7080d7dd2aadf0305a9d3ba9c5d9d (diff) | |
Suggest Set Injection On Proofs in error message for injection.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions