From 4112b9f87a555bfc4c3cd06bae652cd2382cad8b Mon Sep 17 00:00:00 2001 From: Andrea Berlingieri Date: Fri, 27 Sep 2019 15:40:44 +0200 Subject: [PATCH] Change Sort.merge (deprecated) with List.merge --- matita/components/ng_extraction/mlutil.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/matita/components/ng_extraction/mlutil.ml b/matita/components/ng_extraction/mlutil.ml index 0d5e89f6e..52881e183 100644 --- a/matita/components/ng_extraction/mlutil.ml +++ b/matita/components/ng_extraction/mlutil.ml @@ -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 -- 2.39.2