WARNING: partial commit (does not compile)

[helm.git] / matita / components / ng_tactics / nTactics.ml

diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml
index 09427a315d6ca3f99b3c57c5091410e09df6c21c..ac3dd00b7fa3b776ff4b139068e05ed7e5d93f77 100644 (file)
--- 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 =