]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/discrimination_tree.ml
ignore used to avoid Y warning
[helm.git] / helm / ocaml / cic / discrimination_tree.ml
index 6e252901631c4465917ea76042f44513378787ac..bab98921df04691b090c6e8e3020de76e5ccf5bb 100644 (file)
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 module DiscriminationTreeIndexing =  
   functor (A:Set.S) -> 
     struct
@@ -218,7 +220,7 @@ let remove_index tree equality =
            | pos -> List.fold_right (fun i r -> if r = [] then [i+1] else i::r) pos []
        in
          try
-           let t = subterm_at_pos pos' term in pos'
+           ignore(subterm_at_pos pos' term ); pos'
          with Not_found ->
            let pos, _ =
              List.fold_right