diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-01-21 00:26:59 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-01-21 00:46:06 +0100 |
| commit | c2d053c6f38a54e3083c8726eccb3e73942107b7 (patch) | |
| tree | 2eef9978ece47590799ab97acfe9043e213b8d40 /tactics/tacenv.mli | |
| parent | 9cc95f5a34b9050fe5a869f0fb96da562b45353d (diff) | |
Embedding the index of the ML tactic entry in the Tacexpr AST.
This will allow to get rid of the fragile mechanism of discriminating which
entry to call depending on the dynamic type of its arguments.
Diffstat (limited to 'tactics/tacenv.mli')
| -rw-r--r-- | tactics/tacenv.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 29677fd4c..72b1ca90f 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -51,5 +51,5 @@ type ml_tactic = val register_ml_tactic : ?overwrite:bool -> ml_tactic_name -> ml_tactic -> unit (** Register an external tactic. *) -val interp_ml_tactic : ml_tactic_name -> ml_tactic +val interp_ml_tactic : ml_tactic_entry -> ml_tactic (** Get the named tactic. Raises a user error if it does not exist. *) |