diff options
| author | Arnaud Spiwack | 2014-10-17 16:23:01 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-22 07:31:45 +0200 |
| commit | aa64260119704620540017a23815cd7c40c3cff3 (patch) | |
| tree | 677157e51849510130e868d93193fa8c4b3f1ca2 /dev/base_include | |
| parent | a5a355ec3e9cbbfa28be53b9ba6ef914136b0aba (diff) | |
Proofview: remove a redundant primitive.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions