Tout est deja traite dans Tacinterp

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

3 files changed, 0 insertions, 110 deletions

diff --git a/proofs/macros.ml b/proofs/macros.ml
deleted file mode 100644
index 4a7a826f9..000000000
--- a/proofs/macros.ml
+++ /dev/null
@@ -1,87 +0,0 @@
-
-(* $Id$ *)
-
-open Pp
-open Util
-open Names
-open Term
-open Proof_type
-open Libobject
-open Library
-open Coqast
-open Pcoq
-open Ast
-
-(* The data stored in the table *)
-
-type macro_data = {
-  mac_args : string list;
-  mac_body : Ast.act }
-
-(* Summary and Object declaration *)
-
-type t = macro_data Stringmap.t
-type frozen_t = macro_data Stringmap.t
-
-let mactab = ref Stringmap.empty
-
-let lookup id = Stringmap.find id !mactab
-
-let _ = 
-  let init () = mactab := Stringmap.empty  in
-  let freeze () = !mactab in
-  let unfreeze fs = mactab := fs in
-  Summary.declare_summary "tactic-macro"
-    { Summary.freeze_function   = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function     = init }
-
-let (inMD,outMD) =
-  let add (na,md) = mactab := Stringmap.add na md !mactab in
-  let cache_md (_,(na,md)) = add (na,md) in 
-  let export_md x = Some x in
-  declare_object ("TACTIC-MACRO-DATA",
-                  { cache_function = cache_md;
-		    load_function = (fun _ -> ());
-                    open_function = cache_md;
-                    export_function = export_md })
-
-let add_macro_hint na (ids,body) =
-  if Stringmap.mem na !mactab then errorlabstrm "add_macro_hint"
-    [< 'sTR "There is already a Tactic Macro named "; 'sTR na >];
-  let _ = Lib.add_leaf (id_of_string na) OBJ
-	    (inMD(na,{mac_args = ids; mac_body = body})) in
-  ()
-
-let macro_expand macro_loc macro argcoms = 
-  let md =
-    try 
-      lookup macro
-    with Not_found ->
-      user_err_loc(macro_loc,"macro_expand",
-		   [< 'sTR"Tactic macro ";'sTR macro; 'sPC;
-		      'sTR"not defined" >]) 
-  in
-  let transform = 
-    List.map 
-      (function
-	 | Command c -> c
-	 | _ -> user_err_loc(macro_loc,"macro_expand", 
-			     [<'sTR "The arguments of a tactic macro";
-			       'sPC; 'sTR"must be terms">])) 
-  in
-  let argcoms = transform argcoms in
-  if List.length argcoms <> List.length md.mac_args then 
-    user_err_loc
-      (macro_loc,"macro_expand",
-       [< 'sTR "Tactic macro "; 'sTR macro; 'sPC;
-          'sTR "applied to the wrong number of arguments:"; 'sPC;
-          'iNT (List.length argcoms) ; 'sTR" instead of ";
-          'iNT (List.length md.mac_args) >]);
-  let astb = 
-    List.map2 (fun id argcom -> (id, Vast argcom)) md.mac_args argcoms in
-  match Ast.eval_act macro_loc astb md.mac_body with
-    | Vast ast -> ast
-    | _ -> anomaly "expand_macro : eval_act did not return a Vast"
-
-
diff --git a/proofs/macros.mli b/proofs/macros.mli
deleted file mode 100644
index a237d3fd7..000000000
--- a/proofs/macros.mli
+++ /dev/null
@@ -1,22 +0,0 @@
-
-(* $Id$ *)
-
-(*i*)
-open Names
-open Tacmach
-open Proof_type
-(*i*)
-
-(* This file contains the table of macro tactics. The body of the
-   defined tactics is stored as an ast with variables, which are
-   substituted by the real arguments at calling time.
-   User defined tactics are stored in a separate table so that they
-   are sensible to the Reset and Require commands. *)
-
-type macro_data = {
-  mac_args : string list;
-  mac_body : Ast.act }
-
-val add_macro_hint : string -> string list * Ast.act -> unit
-val lookup         : string -> macro_data 
-val macro_expand   : Coqast.loc -> string -> tactic_arg list -> Coqast.t
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 39630ec38..c2dcf0bec 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -15,7 +15,6 @@ open Names
 open Proof_type
 open Tacmach
 open Tactic_debug
-open Macros
 open Coqast
 open Ast
 open Term