X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Ftacticals.ml;h=b0a9f452eda2fef9b064517aa663a8c1b40eb3ae;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=8281c9452e7035bd958f579bef38474810e21302;hpb=097b7147a9daf37360fa51828e0f14843b5bd881;p=helm.git

diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml
index 8281c9452..b0a9f452e 100644
--- a/helm/ocaml/tactics/tacticals.ml
+++ b/helm/ocaml/tactics/tacticals.ml
@@ -315,7 +315,7 @@ struct
   let mk_tactic f =
     ProofEngineTypes.mk_tactic
       (fun (proof, goal) as pstatus ->
-        let stack = [ [ 1, Stack.Open goal ], [], [], Stack.NoTag ] in
+        let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
         let istatus = pstatus, stack in
 (*         let ostatus = f istatus in
         let ((proof, opened, _), _) = ostatus in *)