aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-04 16:45:52 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-04 16:45:52 +0100
commit0a9a45abbd3421f3b2cfc4f6428938898a933ffe (patch)
tree3e1bfbf03731517c48f96b91c3318ed4d0744aca /configure.ml
parentd28726426b048c9c4d521774f6540596a33165c4 (diff)
parent30455aa6d2c1a069abbab7092aeb6096ce84446f (diff)
Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coretactics.ml4.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions