From 9ede7b4e8319516aee4df9dc0ddfd13040049877 Mon Sep 17 00:00:00 2001 From: delahaye Date: Tue, 9 Jan 2001 16:30:04 +0000 Subject: Meta Definition + Tactic Definition git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1240 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/tacinterp.ml | 14 ++++++++------ proofs/tacinterp.mli | 4 ++-- 2 files changed, 10 insertions(+), 8 deletions(-) (limited to 'proofs') 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 -- cgit v1.2.3