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
23 val try_tac: NTacStatus.tactic -> NTacStatus.tactic
25 val distribute_tac: NTacStatus.lowtactic -> NTacStatus.tactic
26 val block_tac: NTacStatus.tactic list -> NTacStatus.tactic
28 val apply_tac: NTacStatus.tactic_term -> NTacStatus.tactic
29 val assumption_tac: NTacStatus.tactic
31 where:NTacStatus.tactic_pattern -> with_what:NTacStatus.tactic_term ->
34 what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
36 val intro_tac: string -> NTacStatus.tactic
38 what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
40 val case1_tac: string -> NTacStatus.tactic
42 dir:[ `LeftToRight | `RightToLeft ] ->
43 what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
45 val generalize_tac : where:NTacStatus.tactic_pattern -> NTacStatus.tactic
47 reduction:[ `Normalize of bool | `Whd of bool ] ->
48 where:NTacStatus.tactic_pattern -> NTacStatus.tactic
50 where:NTacStatus.tactic_pattern ->
51 what: NTacStatus.tactic_term ->
52 string -> NTacStatus.tactic
54 ((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list ->
58 params:(NTacStatus.tactic_term list * (string * string) list) ->