X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTactics.ml;fp=matita%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=ac3dd00b7fa3b776ff4b139068e05ed7e5d93f77;hb=aab0401db0bedd941da96a32acd600af3fbe42e7;hp=09427a315d6ca3f99b3c57c5091410e09df6c21c;hpb=3ce27112fe93ced5f67cc6af8fc63037eba3f322;p=helm.git

diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml
index 09427a315..ac3dd00b7 100644
--- a/matita/components/ng_tactics/nTactics.ml
+++ b/matita/components/ng_tactics/nTactics.ml
@@ -249,7 +249,7 @@ let distribute_tac tac (status : #tac_status) =
        ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn
 ;;
 
-let atomic_tac htac : #tac_status as 'a -> 'a = distribute_tac (exec htac) ;;
+let atomic_tac htac: #tac_status as 'a -> 'a = distribute_tac (exec htac) ;;
 
 let repeat_tac t s = 
   let rec repeat t (status : #tac_status as 'a) : 'a =