Meta Definition + Tactic Definition

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1240 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 29 insertions, 23 deletions

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 0ee8c7aec1..207c624974 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -25,6 +25,10 @@ GEXTEND Gram
   [ [ -> []
     | ":"; l = LIST1 identarg -> l ] ]
   ;
+  deftok:
+    [ [ IDENT "Meta"
+      | IDENT "Tactic" ] ]
+  ;
   vrec_clause:
     [ [ name=identarg; it=LIST1 input_fun; ":="; body=tactic_expr ->
           <:ast<(RECCLAUSE $name (FUNVAR ($LIST $it)) $body)>> ] ]
@@ -85,20 +89,20 @@ GEXTEND Gram
       | IDENT "Show"; IDENT "Tree"; "." -> <:ast< (ShowTree) >>
       | IDENT "Show"; IDENT "Conjectures"; "." -> <:ast< (ShowProofs) >>
 
-(* Meta Definition *)
+(* Definitions for tactics *)
 
-      |IDENT "Meta"; "Definition"; name=identarg; ":="; body=Tactic.tactic;
-        "." -> <:ast<(METADEF $name (AST $body))>>
-      |IDENT "Meta"; "Definition"; name=identarg; largs=LIST1 input_fun;
+      | deftok; "Definition"; name=identarg; ":="; body=Tactic.tactic;
+        "." -> <:ast<(TACDEF $name (AST $body))>>
+      | deftok; "Definition"; name=identarg; largs=LIST1 input_fun;
         ":="; body=Tactic.tactic; "." ->
-        <:ast<(METADEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>>
-      |IDENT "Recursive"; IDENT "Meta"; "Definition"; vc=vrec_clause ; "." ->
+        <:ast<(TACDEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>>
+      | IDENT "Recursive"; deftok; "Definition"; vc=vrec_clause ; "." ->
         (match vc with
             Coqast.Node(_,"RECCLAUSE",nme::tl) ->
-              <:ast<(METADEF $nme (AST (REC $vc)))>>
+              <:ast<(TACDEF $nme (AST (REC $vc)))>>
            |_ ->
              anomalylabstrm "Gram.vernac" [<'sTR "Not a correct RECCLAUSE">])
-      |IDENT "Recursive"; IDENT "Meta"; "Definition"; vc=vrec_clause;
+      |IDENT "Recursive"; deftok; "Definition"; vc=vrec_clause;
         IDENT "And"; vcl=LIST1 vrec_clause SEP IDENT "And"; "." ->
         let nvcl=
           List.fold_right
@@ -109,7 +113,7 @@ GEXTEND Gram
                  anomalylabstrm "Gram.vernac" [<'sTR
                    "Not a correct RECCLAUSE">]) (vc::vcl) []
         in
-          <:ast<(METADEF ($LIST $nvcl))>>
+          <:ast<(TACDEF ($LIST $nvcl))>>
 
 (* Hints for Auto and EAuto *)
 
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 5d7c46a792..8f85384e1a 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 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
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 361cf3d20c..f5599792e8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1342,16 +1342,16 @@ let _ =
        | _ -> bad_vernac_args "SYNTAX")
     
 let _ =
-  add "METADEF"
-    (let rec metadef_fun lacc=function
+  add "TACDEF"
+    (let rec tacdef_fun lacc=function
         (VARG_IDENTIFIER name)::(VARG_AST tacexp)::tl ->
-          metadef_fun ((string_of_id name,tacexp)::lacc) tl
+          tacdef_fun ((string_of_id name,tacexp)::lacc) tl
        |[] ->
          fun () ->
-           List.iter (fun (name,ve) -> Tacinterp.add_metadef name ve) lacc
-       |_ -> bad_vernac_args "METADEF"
+           List.iter (fun (name,ve) -> Tacinterp.add_tacdef name ve) lacc
+       |_ -> bad_vernac_args "TACDEF"
      in
-       metadef_fun [])
+     tacdef_fun [])
 
 let _ =
   add "INFIX"