aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/Init.v
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-07 16:00:58 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-02-07 16:00:58 +0100
commit47e43e229ab02a4dedc2405fed3960a4bf476b58 (patch)
treec819b17483f7faf228669cba93f6b1bf7ce22367 /theories/Classes/Init.v
parenta15ae330fd156b74fcdfb4fc39b79013d3e398bf (diff)
parent0552482c947966f720e265e95db44c45331f38a1 (diff)
Merge PR #6657: Document the Fail command
Diffstat (limited to 'theories/Classes/Init.v')
0 files changed, 0 insertions, 0 deletions