ignore used to avoid Y warning

diff --git a/helm/ocaml/cic/discrimination_tree.ml b/helm/ocaml/cic/discrimination_tree.ml
index 0bef85a8cc4e7ea1d89c3f708c025c0c998cb545..bab98921df04691b090c6e8e3020de76e5ccf5bb 100644 (file)
--- a/helm/ocaml/cic/discrimination_tree.ml
+++ b/helm/ocaml/cic/discrimination_tree.ml
@@ -220,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