]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/tacticals.ml
Added Decompose tactic
[helm.git] / helm / gTopLevel / tacticals.ml
index d48b6a02c28dc5e2ca60876aeaa26a93f288c351..1319c13ca2dc34fa1e20299f0be540fab22c6df0 100644 (file)
@@ -103,7 +103,8 @@ let then_ ~start ~continuation ~status =
 
 
 (* Galla *)
-(* si suppone che tutte le tattiche sollevano solamente Fail? *)
+(* si suppone che tutte le tattiche sollevino solamente Fail? *)
+
 
 (* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *)
 
@@ -201,6 +202,10 @@ let rec solve_tactics ~(tactics: (string * tactic) list) ~status =
 
 
 
+
+
+
+
   (** tattica di prova per debuggare i tatticali *)
 (*
 let thens' ~start ~continuations ~status =