aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-15 22:32:31 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-15 22:32:31 +0200
commit8c5d14bd399a02d15d46a27f14b7791afb30c3c5 (patch)
treee3ed51bbd237cb341b70ee599b5cbd041f433cf7 /interp/notation.ml
parentcd3a834754449e9e554a4878ed5f318475434c38 (diff)
parent36f3ae391ee188edb9d858d8832d7fd611db0482 (diff)
Merge PR#440: Univs: fix bug #5365, generation of u+k <= v constraints
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions