((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 =
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
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 {
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
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)
;;
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