(***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* bs.stack <- e :: bs.stack | Some d -> bs.stack <- fst(safe_chop_list d (e :: bs.stack)) let pop bs = match bs.stack with | [] -> None | h::tl -> (bs.stack <- tl; Some h) let top bs = match bs.stack with | [] -> None | h::_ -> Some h let app_push bs f = match bs.stack with | [] -> error "Nothing on the stack" | h::_ -> push bs (f h) let app_repl bs f = match bs.stack with | [] -> error "Nothing on the stack" | h::t -> bs.stack <- (f h)::t let is_empty bs = bs.stack = [] let depth bs = List.length bs.stack