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/tacintern.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/tacintern.mli')
| -rw-r--r-- | tactics/tacintern.mli | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli index 98d70ce10..c04b6f391 100644 --- a/tactics/tacintern.mli +++ b/tactics/tacintern.mli @@ -61,14 +61,6 @@ val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument -(** Adds a definition of tactics in the table *) -val add_tacdef : - Vernacexpr.locality_flag -> bool -> - (Libnames.reference * bool * raw_tactic_expr) list -> unit -val add_primitive_tactic : string -> glob_tactic_expr -> unit - -val lookup_ltacref : ltac_constant -> glob_tactic_expr - (** printing *) val print_ltac : Libnames.qualid -> std_ppcmds @@ -77,5 +69,8 @@ val print_ltac : Libnames.qualid -> std_ppcmds val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr val dump_glob_red_expr : raw_red_expr -> unit -(* Implemented in tacinterp *) -val set_assert_tactic_installed : (string -> unit) -> unit +(* Hooks *) +val assert_tactic_installed_hook : (string -> unit) Hook.t +val interp_atomic_ltac_hook : (Id.t -> glob_tactic_expr) Hook.t +val interp_ltac_hook : (KerName.t -> glob_tactic_expr) Hook.t +val strict_check : bool ref |