diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-10 22:00:23 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-10 22:00:23 +0000 |
| commit | bf33614eef6c26c169ab9dae9fd2f3713d19d23f (patch) | |
| tree | 177d28a9dc0be4b918f0b2732bcc3adb0db197e9 /tactics/tacinterp.mli | |
| parent | 6544bd19001a18aea49c30e94a09649f2dcc61e4 (diff) | |
Centralizing the Ltac-defining functions in Tacenv.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17080 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index ce6639d4b..64e945b84 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -49,14 +49,6 @@ val extract_ltac_constr_values : interp_sign -> Environ.env -> (** Given an interpretation signature, extract all values which are coercible to a [constr]. *) -(** Tactic extensions *) -val add_tactic : - string -> (typed_generic_argument list -> interp_sign -> unit Proofview.tactic) -> unit -val overwriting_add_tactic : - string -> (typed_generic_argument list -> interp_sign -> unit Proofview.tactic) -> unit -val lookup_tactic : - string -> (typed_generic_argument list) -> interp_sign -> unit Proofview.tactic - (** To embed several objects in Coqast.t *) val tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t val tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr) |