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
36 what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
38 val case1_tac: string -> NTacStatus.tactic
40 dir:[ `LeftToRight | `RightToLeft ] ->
41 what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
43 val generalize_tac : where:NTacStatus.tactic_pattern -> NTacStatus.tactic
45 reduction:[ `Normalize of bool | `Whd of bool ] ->
46 where:NTacStatus.tactic_pattern -> NTacStatus.tactic
48 where:NTacStatus.tactic_pattern ->
49 what: NTacStatus.tactic_term ->
50 string -> NTacStatus.tactic
52 ((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list ->
56 params:'a -> NTacStatus.tactic