X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fng_extraction%2Fmlutil.ml;fp=matita%2Fcomponents%2Fng_extraction%2Fmlutil.ml;h=9f553762a7ccee8707de121ea96e1106f8e017af;hp=01a0cd85def0f5657fe94402ec9133353062257c;hb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;hpb=f00a612006ac05f49a42ab507a95d3298bc1457a

diff --git a/matita/components/ng_extraction/mlutil.ml b/matita/components/ng_extraction/mlutil.ml
index 01a0cd85d..9f553762a 100644
--- a/matita/components/ng_extraction/mlutil.ml
+++ b/matita/components/ng_extraction/mlutil.ml
@@ -1242,7 +1242,7 @@ and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l*)
 	   let n = List.length i in
 	   let cand = lift n cand in
 	   let cand = pop n (non_stricts add cand t) in
-	   List.merge (compare) cand c) [] v
+	   List.merge (-) cand c) [] v
 	(* [merge] may duplicates some indices, but I don't mind. *)
   | MLmagic t ->
       non_stricts add cand t