2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
14 val dot_tac: NTacStatus.tactic
15 val branch_tac: NTacStatus.tactic
16 val shift_tac: NTacStatus.tactic
17 val pos_tac: int list -> NTacStatus.tactic
18 val wildcard_tac: NTacStatus.tactic
19 val merge_tac: NTacStatus.tactic
20 val focus_tac: int list -> NTacStatus.tactic
21 val unfocus_tac: NTacStatus.tactic
22 val skip_tac: NTacStatus.tactic
24 val distribute_tac: NTacStatus.lowtactic -> NTacStatus.tactic
25 val block_tac: NTacStatus.tactic list -> NTacStatus.tactic
27 val apply_tac: NTacStatus.tactic_term -> NTacStatus.tactic
29 where:NTacStatus.tactic_pattern -> with_what:NTacStatus.tactic_term ->
32 what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
34 val intro_tac: string -> NTacStatus.tactic
35 val case1_tac: string -> NTacStatus.tactic