X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTactics.ml;fp=matita%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=721d9165b7d32d0388ba084d32fa27b6ff672125;hp=a8a78999a2b9c3b71a4ea20a93ffab8250d870d0;hb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;hpb=4112b9f87a555bfc4c3cd06bae652cd2382cad8b

diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml
index a8a78999a..721d9165b 100644
--- a/matita/components/ng_tactics/nTactics.ml
+++ b/matita/components/ng_tactics/nTactics.ml
@@ -312,7 +312,7 @@ let assumption_tac status = distribute_tac (fun status goal ->
 let find_in_context name context =
   let rec aux acc = function
     | [] -> raise Not_found
-    | (hd,_) :: tl when hd = name -> acc
+    | (hd,_) :: _ when hd = name -> acc
     | _ :: tl ->  aux (acc + 1) tl
   in
   aux 1 context
@@ -503,7 +503,7 @@ let analyze_indty_tac ~what indtyref =
   let goalty = get_goalty status goal in
   let status, what = disambiguate status (ctx_of goalty) what `XTInd in
   let status, ty_what = typeof status (ctx_of what) what in 
-  let status, (r,consno,lefts,rights,cl) = analyse_indty status ty_what in
+  let _status, (r,consno,lefts,rights,cl) = analyse_indty status ty_what in
   let leftno = List.length lefts in
   let rightno = List.length rights in
   indtyref := Some { 
@@ -704,7 +704,7 @@ let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
 let assert_tac seqs status =
  match status#stack with
   | [] -> assert false
-  | (g,_,_,_,_) :: s ->
+  | (g,_,_,_,_) :: _s ->
      assert (List.length g = List.length seqs);
      (match seqs with
          [] -> id_tac