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 $ *)
15 type lowtac_status = {
17 lstatus : LexiconEngine.status
20 type lowtactic = lowtac_status * int -> lowtac_status * int list * int list
23 gstatus : Continuationals.Stack.t;
24 istatus : lowtac_status;
27 type tactic = tac_status -> tac_status
29 type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
32 val branch_tac: tactic
34 val pos_tac: int list -> tactic
35 val wildcard_tac: tactic
37 val focus_tac: int list -> tactic
38 val unfocus_tac: tactic
41 val distribute_tac: lowtactic -> tactic
42 val block_tac: tactic list -> tactic
44 val apply_tac: tactic_term -> tactic
47 val pp_tac_status: tac_status -> unit