diff options
| author | Gaëtan Gilbert | 2018-09-11 23:44:54 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-19 13:15:54 +0200 |
| commit | 448a1dd0763a36eddf52ee2feadf93479d34b347 (patch) | |
| tree | 5f201308585e38592589d2474fd93aa20bc92fea /dev/ci/docker | |
| parent | 11a748d42dbf8536abceccbedc350806fcdab8eb (diff) | |
Replace trivial uses of declare_summary with summary.refs
The one in notation.ml looks trivial but is needed to do
with_notation_protection (used by inductive/fixpoint local notations).
Diffstat (limited to 'dev/ci/docker')
0 files changed, 0 insertions, 0 deletions