aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/goptions.ml
diff options
context:
space:
mode:
authorGravatar Matej Kosik <matej.kosik@inria.fr>2016-11-05 16:29:54 +0100
committerGravatar Matej Kosik <matej.kosik@inria.fr>2016-11-05 16:29:54 +0100
commit0f5e89ec54bc613f59ce971e6a95ed1161ffc37b (patch)
tree55ab1b62b34b3ae4b4aae19f3b9030f1a4a04b67 /library/goptions.ml
parentbeb5875cca7648ba9963c99a68ea22494ab6329b (diff)
parent6b99de706e37c75407373e756e24f2256b848815 (diff)
Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr/gitroot/coq/coq into trunk
Diffstat (limited to 'library/goptions.ml')
0 files changed, 0 insertions, 0 deletions