aboutsummaryrefslogtreecommitdiff
path: root/API/API.mli
diff options
context:
space:
mode:
authorSam Pablo Kuper2017-08-03 19:43:22 +0100
committerSam Pablo Kuper2017-08-03 19:43:22 +0100
commit27498bb9efcd6cefe7847595be4a61a033c84266 (patch)
treeba6e9a6d75f567f4737c8088364d6a4c392db496 /API/API.mli
parenteee42a2403f5bdcf97139deb97f9cd0a7a434ddc (diff)
Amend wording to capture intended meaning
per @Zimmi48's comments [here](https://github.com/coq/coq/pull/944#discussion_r131072333) and [here](https://github.com/coq/coq/pull/944#discussion_r131072790).
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions