aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Vectors
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-08-28 09:39:30 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-09-08 12:45:58 +0200
commit108ede6e7aa4383474581bc428ff05b94097c92d (patch)
tree4315c802d37b99196338eadfb2e410d8bf410027 /theories/Vectors
parent0f8d1b92c37c80e96df2a157a78188d6d94b6e35 (diff)
Documenting the code when preference is given to expansion of default
clause in pattern-matching or not.
Diffstat (limited to 'theories/Vectors')
0 files changed, 0 insertions, 0 deletions