Meta Definition + Tactic Definition

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

1 files changed, 6 insertions, 6 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 361cf3d20..f5599792e 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"