aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/envars.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-01-05 17:03:37 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2017-05-23 10:48:27 +0200
commitda5ac9169d0c65ff389104dfd983311b85e059e2 (patch)
tree135a0285b1042779b41d3af5a7897d5ef3cfa95b /lib/envars.ml
parent088ddea70d2d9121d76f0f3c6c0412fd2a67ff0a (diff)
CoqProject_file: document in API deprecated features
Diffstat (limited to 'lib/envars.ml')
0 files changed, 0 insertions, 0 deletions