- added HBugs notification after tactic application

[helm.git] / helm / gTopLevel / invokeTactics.mli

diff --git a/helm/gTopLevel/invokeTactics.mli b/helm/gTopLevel/invokeTactics.mli
index 313991cedd21f41679e270d759f67c0356302d2d..11b8ecf72c9960d40e7cd9cc3c21f9afae7a7642 100644 (file)
--- a/helm/gTopLevel/invokeTactics.mli
+++ b/helm/gTopLevel/invokeTactics.mli
@@ -62,46 +62,50 @@ module type Callbacks =
       (UriManager.uri * int * 'b list) list
     val mk_fresh_name_callback :
       Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
+    val notify_hbugs : unit -> unit
   end
 
-module Make (C : Callbacks) :
+module type Tactics =
  sig
    val intros : unit -> unit
-   val exact : unit -> unit
-   val apply : unit -> unit
-   val elimintrossimpl : unit -> unit
-   val elimtype : unit -> unit
+   val exact : ?term:string -> unit -> unit
+   val apply : ?term:string -> unit -> unit
+   val elimintrossimpl : ?term:string -> unit -> unit
+   val elimtype : ?term:string -> unit -> unit
    val whd : unit -> unit
    val reduce : unit -> unit
    val simpl : unit -> unit
-   val fold_whd : unit -> unit
-   val fold_reduce : unit -> unit
-   val fold_simpl : unit -> unit
-   val cut : unit -> unit
+   val fold_whd : ?term:string -> unit -> unit
+   val fold_reduce : ?term:string -> unit -> unit
+   val fold_simpl : ?term:string -> unit -> unit
+   val cut : ?term:string -> unit -> unit
    val change : unit -> unit
-   val letin : unit -> unit
+   val letin : ?term:string -> unit -> unit
    val ring : unit -> unit
    val clearbody : unit -> unit
    val clear : unit -> unit
    val fourier : unit -> unit
-   val rewritesimpl : unit -> unit
-   val rewritebacksimpl : unit -> unit
+   val rewritesimpl : ?term:string -> unit -> unit
+   val rewritebacksimpl : ?term:string -> unit -> unit
    val replace : unit -> unit
    val reflexivity : unit -> unit
    val symmetry : unit -> unit
-   val transitivity : unit -> unit
+   val transitivity : ?term:string -> unit -> unit
    val exists : unit -> unit
    val split : unit -> unit
    val left : unit -> unit
    val right : unit -> unit
    val assumption : unit -> unit
    val generalize : unit -> unit
-   val absurd : unit -> unit
+   val absurd : ?term:string -> unit -> unit
    val contradiction : unit -> unit
-   val decompose : unit -> unit
-   val injection : unit -> unit
-   val discriminate : unit -> unit
+   val decompose : ?term:string -> unit -> unit
+   val injection : ?term:string -> unit -> unit
+   val discriminate : ?term:string -> unit -> unit
    val whd_in_scratch : unit -> unit
    val reduce_in_scratch : unit -> unit
    val simpl_in_scratch : unit -> unit
  end
+
+module Make (C : Callbacks) : Tactics
+