Merge branch 'declarative' into matita-lablgtk3

[helm.git] / matita / components / ng_extraction / mlutil.ml

diff --git a/matita/components/ng_extraction/mlutil.ml b/matita/components/ng_extraction/mlutil.ml
index 01a0cd85def0f5657fe94402ec9133353062257c..9f553762a7ccee8707de121ea96e1106f8e017af 100644 (file)
--- 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