]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/tacticAst2Box.mli
embedded commands ast into tacticals ast
[helm.git] / helm / ocaml / cic_transformations / tacticAst2Box.mli
index 36eeb3e73f654fb2fab8dccdfd742b954a9137bd..0eeef6c533a676777ac64632721d30f9987884d6 100644 (file)
@@ -34,9 +34,8 @@
 
 
 val tactical2box:
-  ?attr:'a list 
-  -> (CicAst.term, string) TacticAst.tactic TacticAst.tactical 
-  -> CicAst.term Box.box
+  ?attr:'a list -> (CicAst.term, string) TacticAst.tactical ->
+    CicAst.term Box.box
+
+val tacticalPp: (CicAst.term, string) TacticAst.tactical -> string
 
-val tacticalPp:
-  (CicAst.term, string) TacticAst.tactic TacticAst.tactical -> string