aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-10-09 09:48:48 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-10-09 09:48:53 +0200
commit73daf37ccc7a44cd29c9b67405111756c75cb26a (patch)
tree5ebc5d9e3e27eb34f5714a33ba957fce621b3659 /kernel/univ.mli
parentb6edcae7b61ea6ccc0e65223cecb71cab0dd55cc (diff)
Remove misleading warning (Close #4365)
Diffstat (limited to 'kernel/univ.mli')
0 files changed, 0 insertions, 0 deletions