aboutsummaryrefslogtreecommitdiff
path: root/measurements
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <maxime.denes@inria.fr>2019-01-02 15:21:55 +0100
committerGravatar Jason Gross <jasongross9@gmail.com>2019-01-02 17:43:36 -0500
commit2238baafd6ad626bbec17b85cbeb79f848475d6e (patch)
tree0395665538d8b330d918c6e37f3b74485774f4a4 /measurements
parentcd7cb6081acb9089337c5c65f0f985034a8091d3 (diff)
Do not rely on `Refine Instance Mode`
This option is soon going to be turned off by default. See https://github.com/coq/coq/pull/9270
Diffstat (limited to 'measurements')
0 files changed, 0 insertions, 0 deletions