aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-01-09 16:30:04 +0000
committerGravatar delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-01-09 16:30:04 +0000
commit9ede7b4e8319516aee4df9dc0ddfd13040049877 (patch)
treeb2a61ff2d8aae1049c9315af5023f02196008845 /proofs
parentdfe152b89af9239899e32b2a31adbfda44af5efe (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')
-rw-r--r--proofs/tacinterp.ml14
-rw-r--r--proofs/tacinterp.mli4
2 files changed, 10 insertions, 8 deletions
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 5d7c46a79..8f85384e1 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -1117,24 +1117,26 @@ let bad_tactic_args s =
anomalylabstrm s
[<'sTR "Tactic "; 'sTR s; 'sTR " called with bad arguments">]
-(* Declaration of the META-DEFINITION object *)
+(* Declaration of the TAC-DEFINITION object *)
let (inMD,outMD) =
let add (na,td) = mactab := Gmap.add na td !mactab in
let cache_md (_,(na,td)) =
let ve=val_interp (Evd.empty,Environ.empty_env,[],[],None,get_debug ()) td
in add (na,ve) in
- declare_object ("META-DEFINITION",
+ declare_object ("TAC-DEFINITION",
{cache_function = cache_md;
load_function = (fun _ -> ());
open_function = cache_md;
export_function = (fun x -> Some x)})
-(* Adds a Meta Definition in the table *)
-let add_metadef na vbody =
+(* Adds a definition for tactics in the table *)
+let add_tacdef na vbody =
begin
if Gmap.mem na !mactab then
- errorlabstrm "Tacinterp.add_metadef"
- [<'sTR "There is already a Meta Definition named "; 'sTR na>];
+ errorlabstrm "Tacinterp.add_tacdef"
+ [< 'sTR
+ "There is already a Meta Definition or a Tactic Definition named ";
+ 'sTR na>];
let _ = Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) in
if Options.is_verbose() then mSGNL [< 'sTR (na ^ " is defined") >]
end
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 67bd209e3..83cd7be1c 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