module Macros et Tacinterp

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@115 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 24 insertions, 0 deletions

diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
new file mode 100644
index 0000000000..5dbad51769
--- /dev/null
+++ b/proofs/tacinterp.mli
@@ -0,0 +1,24 @@
+
+(* $Id$ *)
+
+(*i*)
+open Pp
+open Names
+open Proof_trees
+open Tacmach
+open Term
+(*i*)
+
+(* Interpretation of tactics. *)
+
+val tacinterp_add        : string * (tactic_arg list -> tactic) -> unit
+val tacinterp_map        : string -> tactic_arg list -> tactic
+val tacinterp_init       : unit -> unit
+val interp               : Coqast.t -> tactic
+val interp_atomic        : Coqast.loc -> string -> tactic_arg list -> tactic
+val interp_semi_list     : tactic -> Coqast.t list -> tactic
+val vernac_interp        : Coqast.t -> tactic
+val vernac_interp_atomic : identifier -> tactic_arg list -> tactic
+val overwriting_tacinterp_add : string * (tactic_arg list -> tactic) -> unit
+val is_just_undef_macro     : Coqast.t -> string option
+