X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Fast.mli;h=3a528ea200fcb47d53ea86d8ef45a33a5312aed8;hb=84972c63d0dbc5a0da05ae08a5b99a9ad81baadc;hp=e47ddc35fd1b65c5770e74fef64eb38b5c83a6bb;hpb=0a41019f02474e4819ecdd739814b849bc58b84e;p=goals.git

diff --git a/src/ast.mli b/src/ast.mli
index e47ddc3..3a528ea 100644
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -87,22 +87,6 @@ val getgoal : env -> loc -> id -> goal
     found or if the named variable is not a tactic. *)
 val gettactic : env -> loc -> id -> tactic
 
-(** Take any expression and simplify it down to a constant.
-    If the expression cannot be simplified then this raises
-    [Failure _]. *)
-val to_constant : env -> expr -> constant
-
-(** Take a substitution list and try to turn it into a simple
-    string by evaluating every variable.  If not possible this
-    raises [Failure _]. *)
-val substitute : env -> loc -> substs -> string
-
-(** Similar to {!substitute} except this is used where we will
-    pass the result immediately to the shell to execute.  Variables
-    are substituted with shell quoted strings.  Raises [Failure _]
-    on error. *)
-val to_shell_script : env -> loc -> substs -> string
-
 (** This is used for incrementally building Ast.substs in the parser. *)
 module Substs : sig
   type t