...

[helm.git] / helm / software / components / ng_tactics / nTactics.mli

diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli
index 831704924ab46539d1d891c0144ac7afed8a9927..de8c24738b1e3d177073961a7672f16e9532ac89 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.mli
+++ b/helm/software/components/ng_tactics/nTactics.mli
@@ -11,13 +11,14 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
+exception Error of string lazy_t
 
 type lowtac_status = {
         pstatus : NCic.obj;
         lstatus : LexiconEngine.status
 }
 
-type lowtactic = lowtac_status * int -> lowtac_status * int list * int list
+type lowtactic = lowtac_status -> int -> lowtac_status
 
 type tac_status = {
         gstatus : Continuationals.Stack.t; 
@@ -27,6 +28,7 @@ type tac_status = {
 type tactic = tac_status -> tac_status
 
 type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
+type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
 
 val dot_tac: tactic
 val branch_tac: tactic
@@ -38,9 +40,12 @@ val focus_tac: int list -> tactic
 val unfocus_tac: tactic
 val skip_tac: tactic
 
-val fold_tactic: lowtactic -> tactic
+val distribute_tac: lowtactic -> tactic
+val block_tac: tactic list -> tactic
 
 val apply_tac: tactic_term -> tactic
-
+val change_tac: where:tactic_pattern -> with_what:tactic_term -> tactic
+val elim_tac: what:tactic_term -> where:tactic_pattern -> tactic
+val intro_tac: string -> tactic
 
 val pp_tac_status: tac_status -> unit