X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_extraction%2Fmlutil.ml;h=52881e18336f3b1f2e6fd7c512355afbf6bc7e24;hb=4112b9f87a555bfc4c3cd06bae652cd2382cad8b;hp=0d5e89f6e0962b5815c97ee3dda719c172ce8371;hpb=95e3387af669e9a9e30dafd4d096c2741fc9041c;p=helm.git

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