]> matita.cs.unibo.it Git - helm.git/commit
Change Sort.merge (deprecated) with List.merge
authorAndrea Berlingieri <andrea.berlingieri42@gmail.com>
Fri, 27 Sep 2019 13:40:44 +0000 (15:40 +0200)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 27 Sep 2019 13:58:08 +0000 (15:58 +0200)
commit4112b9f87a555bfc4c3cd06bae652cd2382cad8b
treeb0aaeb6fa4fcc9988d0d97a18ac0d87d85089e6c
parentaad5588b82d0f2991c336f7ac2f3fadd76768eeb
Change Sort.merge (deprecated) with List.merge
matita/components/ng_extraction/mlutil.ml