]> matita.cs.unibo.it Git - helm.git/commitdiff
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)
matita/components/ng_extraction/mlutil.ml

index 0d5e89f6e0962b5815c97ee3dda719c172ce8371..52881e18336f3b1f2e6fd7c512355afbf6bc7e24 100644 (file)
@@ -1242,7 +1242,7 @@ let rec non_stricts add cand = function
           let n = List.length i in
           let cand = lift n cand in
           let cand = pop n (non_stricts add cand t) in
-          Sort.merge (<=) cand c) [] v
+       List.merge (fun c1 c2 -> c1 - c2) cand c) [] v
        (* [merge] may duplicates some indices, but I don't mind. *)
   | MLmagic t ->
       non_stricts add cand t