diff options
author | 2006-09-26 11:18:22 +0000 | |
---|---|---|
committer | 2006-09-26 11:18:22 +0000 | |
commit | 351a500eada776832ac9b09657e42f5d6cd7210f (patch) | |
tree | af45a745540e1154eab8955c17e03cbbe2e6b878 /tactics/tacinterp.mli | |
parent | 5155de9ee4bd01127a57c36cebbd01c5d903d048 (diff) |
mise a jour du nouveau ring et ajout du nouveau field, avant renommages
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacinterp.mli')
-rw-r--r-- | tactics/tacinterp.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index f343bc949..ca9b076d9 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -64,6 +64,14 @@ val add_tacdef : bool -> (identifier Util.located * raw_tactic_expr) list -> unit val add_primitive_tactic : string -> glob_tactic_expr -> unit +(* Tactic extensions *) +val add_tactic : + string -> (closed_generic_argument list -> tactic) -> unit +val overwriting_add_tactic : + string -> (closed_generic_argument list -> tactic) -> unit +val lookup_tactic : + string -> (closed_generic_argument list) -> tactic + (* Adds an interpretation function for extra generic arguments *) type glob_sign = { ltacvars : identifier list * identifier list; |