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: 's NTacStatus.tactic
15 val branch_tac: 's NTacStatus.tactic
16 val shift_tac: 's NTacStatus.tactic
17 val pos_tac: int list -> 's NTacStatus.tactic
18 val wildcard_tac: 's NTacStatus.tactic
19 val merge_tac: 's NTacStatus.tactic
20 val focus_tac: int list -> 's NTacStatus.tactic
21 val unfocus_tac: 's NTacStatus.tactic
22 val skip_tac: 's NTacStatus.tactic
23 val try_tac: 's NTacStatus.tactic -> 's NTacStatus.tactic
24 val repeat_tac: NTacStatus.tac_status NTacStatus.tactic -> 's NTacStatus.tactic
27 NTacStatus.lowtac_status NTacStatus.lowtactic -> 's NTacStatus.tactic
28 val block_tac: 's NTacStatus.tactic list -> 's NTacStatus.tactic
30 val apply_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic
31 val assumption_tac: 's NTacStatus.tactic
33 where:NTacStatus.tactic_pattern -> with_what:NTacStatus.tactic_term ->
36 what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
38 val intro_tac: string -> 's NTacStatus.tactic
40 what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
42 val case1_tac: string -> 's NTacStatus.tactic
44 dir:[ `LeftToRight | `RightToLeft ] ->
45 what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern ->
47 val generalize_tac : where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic
49 reduction:[ `Normalize of bool | `Whd of bool ] ->
50 where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic
52 where:NTacStatus.tactic_pattern ->
53 what: NTacStatus.tactic_term ->
54 string -> 's NTacStatus.tactic
56 ((string * [`Decl of NTacStatus.tactic_term | `Def of NTacStatus.tactic_term * NTacStatus.tactic_term]) list * NTacStatus.tactic_term) list ->
60 params:(NTacStatus.tactic_term list * (string * string) list) ->