Porting to ocaml 5

[helm.git] / matita / components / ng_paramodulation / stats.ml

diff --git a/matita/components/ng_paramodulation/stats.ml b/matita/components/ng_paramodulation/stats.ml
index fd68f0fe765cd7cd75be5805dac8c516a0f623fb..a1e892902002f8d83f56067888633e3d4bb0a038 100644 (file)
--- a/matita/components/ng_paramodulation/stats.ml
+++ b/matita/components/ng_paramodulation/stats.ml
@@ -115,8 +115,8 @@ module Stats (B : Terms.Blob) =
                            else
                              dependencies op tl acc
                        else dependencies op tl acc
-                    | ((Terms.Node (Terms.Leaf op1::t) as x),y)
-                    | (y,(Terms.Node (Terms.Leaf op1::t) as x)) when leaf_count x > leaf_count y ->
+                    | ((Terms.Node (Terms.Leaf op1::_t) as x),y)
+                    | (y,(Terms.Node (Terms.Leaf op1::_t) as x)) when leaf_count x > leaf_count y ->
                          let rec term_leaves = function
                            | Terms.Node l -> List.fold_left (fun acc x -> acc @ (term_leaves x)) [] l
                            | Terms.Leaf x -> [x]
@@ -129,7 +129,7 @@ module Stats (B : Terms.Blob) =
                    | _ -> dependencies op tl acc
     ;;
 
-    let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));;
+    let dependencies op clauses = HExtlib.list_uniq (List.sort Stdlib.compare (dependencies op clauses []));;
 
     (* let max_weight_hyp = *)