Use of standard OCaml syntax

[helm.git] / matita / components / ng_tactics / nTactics.ml

diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml
index a8a78999a2b9c3b71a4ea20a93ffab8250d870d0..4575133677029d72f4344657d468e0e54c46d658 100644 (file)
--- a/matita/components/ng_tactics/nTactics.ml
+++ b/matita/components/ng_tactics/nTactics.ml
@@ -263,7 +263,7 @@ let distribute_tac tac (status : #tac_status) =
        ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_pstatus sn
 ;;
 
-let atomic_tac htac: #tac_status as 'a -> 'a = distribute_tac (exec htac) ;;
+let atomic_tac htac: (#tac_status as 'a) -> 'a = distribute_tac (exec htac) ;;
 
 let repeat_tac t s = 
   let rec repeat t (status : #tac_status as 'a) : 'a = 
@@ -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 { 
@@ -546,10 +546,7 @@ let pp_cl cl =
     pp_aux cl
 ;;
 
-let pp_indtyinfo ity = "leftno: " ^ (string_of_int ity.leftno) ^ ", consno: " ^ (string_of_int
-                                                                                   ity.consno) ^ ", rightno: " ^
-                       (string_of_int ity.rightno) ^ ", reference: " ^ (pp_ref ity.reference) ^ ",
-                       cl: " ^ (pp_cl ity.cl);;
+let pp_indtyinfo ity = "leftno: " ^ (string_of_int ity.leftno) ^ ", consno: " ^ (string_of_int ity.consno) ^ ", rightno: " ^ (string_of_int ity.rightno) ^ ", reference: " ^ (pp_ref ity.reference) ^ ", cl: " ^ (pp_cl ity.cl);;
 
 let elim_tac ~what:(txt,len,what) ~where = 
   let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
@@ -663,7 +660,7 @@ let constructor_tac ?(num=1) ~args = distribute_tac (fun status goal ->
   let t = 
     if args = [] then Ast.NRef ref else
     Ast.Appl (HExtlib.list_concat ~sep:[Ast.Implicit `Vector]
-      ([Ast.NRef ref] :: List.map (fun _,_,x -> [x]) args))
+      ([Ast.NRef ref] :: List.map (fun (_,_,x) -> [x]) args))
   in
   exec (apply_tac ("",0,t)) status goal)
 ;;
@@ -704,7 +701,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