aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-02-12 21:34:27 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-06-09 15:38:49 +0200
commitc2a9cf2730e5e2d7296449ad0acb406e25aead7f (patch)
treee4e63eb044a0c1b5fd4c8741fba33f4e2d9a90f4 /library/library.ml
parentb9a15a390f34208bd642b0a97a35d32d3b3dfc01 (diff)
Minor simplification in evarconv.ml.
Diffstat (limited to 'library/library.ml')
0 files changed, 0 insertions, 0 deletions