aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/obligations.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-09 15:31:48 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-09 15:31:48 +0100
commit3d86afb36517c9ba4200289e169239f7fa54fca1 (patch)
tree0bb877f733155ac060c1a9d480ce18b35b4fbf72 /vernac/obligations.ml
parent6c43c26a98ea197e9c07b03b76e1916b9f94bb00 (diff)
parent079e895cad0a205e22202da5ba1a919a820c863b (diff)
Merge PR #6947: coqide: queries from the query window are routed there (fix #5684)
Diffstat (limited to 'vernac/obligations.ml')
0 files changed, 0 insertions, 0 deletions