aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-07-21 14:17:59 +0200
committerPierre-Marie Pédrot2014-07-21 14:17:59 +0200
commit2aa92f2da205db588734007f5d68cd1031bb83b5 (patch)
tree2bac2e7ad9e1985ed8b703f7c2b23b993886d426 /library
parent42aa1e96b95f1078a36184c1d2de224fc35dfe2c (diff)
Documenting the change of semantics of the "constructor" tactic.
Diffstat (limited to 'library')
0 files changed, 0 insertions, 0 deletions