diff options
| author | delahaye | 2001-01-09 16:30:04 +0000 |
|---|---|---|
| committer | delahaye | 2001-01-09 16:30:04 +0000 |
| commit | 9ede7b4e8319516aee4df9dc0ddfd13040049877 (patch) | |
| tree | b2a61ff2d8aae1049c9315af5023f02196008845 /proofs/tacinterp.mli | |
| parent | dfe152b89af9239899e32b2a31adbfda44af5efe (diff) | |
Meta Definition + Tactic Definition
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1240 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/tacinterp.mli')
| -rw-r--r-- | proofs/tacinterp.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli index 67bd209e30..83cd7be1c2 100644 --- a/proofs/tacinterp.mli +++ b/proofs/tacinterp.mli @@ -49,8 +49,8 @@ val set_debug : debug_info -> unit (* Gives the state of debug *) val get_debug : unit -> debug_info -(* Adds a Meta Definition in the table *) -val add_metadef : string -> Coqast.t -> unit +(* Adds a definition for tactics in the table *) +val add_tacdef : string -> Coqast.t -> unit (* Interprets any expression *) val val_interp : interp_sign -> Coqast.t -> value |