]> matita.cs.unibo.it Git - helm.git/commitdiff
ignore used to avoid Y warning
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 12 Jan 2006 11:24:17 +0000 (11:24 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 12 Jan 2006 11:24:17 +0000 (11:24 +0000)
helm/ocaml/cic/discrimination_tree.ml

index 0bef85a8cc4e7ea1d89c3f708c025c0c998cb545..bab98921df04691b090c6e8e3020de76e5ccf5bb 100644 (file)
@@ -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