Arite cachee de Match Context + Meta Definition

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

1 files changed, 6 insertions, 6 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9ad4fa012..361cf3d20 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1342,16 +1342,16 @@ let _ =
        | _ -> bad_vernac_args "SYNTAX")
     
 let _ =
-  add "TACDEF"
-    (let rec tacdef_fun lacc=function
+  add "METADEF"
+    (let rec metadef_fun lacc=function
         (VARG_IDENTIFIER name)::(VARG_AST tacexp)::tl ->
-          tacdef_fun ((string_of_id name,tacexp)::lacc) tl
+          metadef_fun ((string_of_id name,tacexp)::lacc) tl
        |[] ->
          fun () ->
-           List.iter (fun (name,ve) -> Tacinterp.add_tacdef name ve) lacc
-       |_ -> bad_vernac_args "TACDEF"
+           List.iter (fun (name,ve) -> Tacinterp.add_metadef name ve) lacc
+       |_ -> bad_vernac_args "METADEF"
      in
-       tacdef_fun [])
+       metadef_fun [])
 
 let _ =
   add "INFIX"