X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_refiner%2FnDiscriminationTree.ml;h=b5338715dfd35936fc8f11f8ea9a89e6bb104c44;hb=HEAD;hp=3c30ce0029749d06c70b7de8e01623dc96701fd9;hpb=040489c7decbea06f923332fee132165b7097145;p=helm.git

diff --git a/matita/components/ng_refiner/nDiscriminationTree.ml b/matita/components/ng_refiner/nDiscriminationTree.ml
index 3c30ce002..b5338715d 100644
--- a/matita/components/ng_refiner/nDiscriminationTree.ml
+++ b/matita/components/ng_refiner/nDiscriminationTree.ml
@@ -29,7 +29,7 @@ open Discrimination_tree
 
 module TermOT : Set.OrderedType with type t = NCic.term = struct 
   type t = NCic.term 
-  let compare = Pervasives.compare 
+  let compare = Stdlib.compare 
 end
 
 module TermSet = Set.Make(TermOT)
@@ -37,7 +37,7 @@ module TermSet = Set.Make(TermOT)
 module TermListOT : Set.OrderedType with type t = NCic.term list =
  struct
    type t = NCic.term list
-   let compare = Pervasives.compare
+   let compare = Stdlib.compare
  end
 
 module TermListSet : Set.S with type elt = NCic.term list =
@@ -65,6 +65,7 @@ let ppelem = function
 let path_string_of t =
   let rec aux arity depth = function
     | NCic.Appl ((NCic.Meta _|NCic.Implicit _)::_) -> [Variable]
+    | NCic.Appl (NCic.Match _::_) -> [Dead]
     | NCic.Appl (NCic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *)
     | NCic.Appl [] -> assert false
     | NCic.Appl l when depth > 10 || List.length l > 50 -> [Variable]
@@ -90,8 +91,8 @@ let compare e1 e2 =
   match e1,e2 with
   | Constant (u1,a1),Constant (u2,a2) -> 
        let x = NReference.compare u1 u2 in
-       if x = 0 then Pervasives.compare a1 a2 else x
-  | e1,e2 -> Pervasives.compare e1 e2
+       if x = 0 then Stdlib.compare a1 a2 else x
+  | e1,e2 -> Stdlib.compare e1 e2
 ;;
 
 let string_of_path l = String.concat "." (List.map ppelem l) ;;