From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 8 Oct 2009 09:48:24 +0000 (+0000)
Subject: avoid warning
X-Git-Tag: make_still_working~3351
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1e7b084682623531f0a4b23618c6614c3a0c0436;p=helm.git

avoid warning
---

diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml
index 1ee47c74e..6fc9b2eee 100644
--- a/helm/software/components/ng_tactics/nInversion.ml
+++ b/helm/software/components/ng_tactics/nInversion.ml
@@ -95,7 +95,7 @@ let mk_inverter name it leftno ?selection outsort status baseuri =
      pp (lazy ("lunghezza rs = " ^ string_of_int (List.length rs)));
      let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (nparams+1)) in
     
-     let id_xs = List.map mk_id xs in
+     let _id_xs = List.map mk_id xs in
      let id_ls = List.map mk_id ls in
      let id_rs = List.map mk_id rs in
      let id_ys = List.map mk_id ys in