diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-11-20 16:04:12 +0100 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-11-20 10:04:12 -0500 |
commit | caa187ddaa5e10f289c59b85844d7bc58817641b (patch) | |
tree | 4c1a4f9bb0d920ab3b74be77ed875e302bbca471 /coqprime/README.md | |
parent | 3d2e80e1c91fd06197236405740e6b115b4addc4 (diff) |
Remove obsolete syntax for locality. (#270)
This is preparing the landing of https://github.com/coq/coq/pull/1049.
For now, I'm duplicating this patch which was already done upstream in
CoqPrime, but please consider removing this ad-hoc copy (see discussion
on PR #269).
Diffstat (limited to 'coqprime/README.md')
0 files changed, 0 insertions, 0 deletions