]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/tacticals.ml
ocaml 3.09 transition
[helm.git] / helm / ocaml / tactics / tacticals.ml
index 8281c9452e7035bd958f579bef38474810e21302..b0a9f452eda2fef9b064517aa663a8c1b40eb3ae 100644 (file)
@@ -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 *)