aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/constr_matching.ml
diff options
context:
space:
mode:
authorGravatar Arnaud Spiwack <arnaud@spiwack.net>2015-10-30 10:06:24 +0100
committerGravatar Arnaud Spiwack <arnaud@spiwack.net>2015-10-30 10:06:24 +0100
commit441ea07e3c8ba56b9e7d44e7802246dc06814415 (patch)
tree6f5b75969e49ab97e4ed1e03f8d09bed68306be5 /pretyping/constr_matching.ml
parent48ffb1173702f86fa6cb6392f7876d7da5e5d6b6 (diff)
More uniformity in the style of comparison functions.
Diffstat (limited to 'pretyping/constr_matching.ml')
0 files changed, 0 insertions, 0 deletions