Ajout du langage de tactiques

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

3 files changed, 25 insertions, 23 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e69d537a1a..7737bdc6ce 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -15,6 +15,7 @@ open Reduction
 open Pfedit
 open Tacmach
 open Proof_trees
+open Proof_type
 open Tacred
 open Library
 open Libobject
@@ -728,10 +729,10 @@ let _ =
 	   let typ_opt,red_option = match rest with
 	     | [] -> None, None
 	     | [VARG_CONSTR t] -> Some t, None
-	     | [VARG_TACTIC_ARG (Redexp(r1,r2))] ->
-		 None, Some (redexp_of_ast Evd.empty (Global.env()) (r1,r2))
-	     | [VARG_CONSTR t; VARG_TACTIC_ARG (Redexp(r1,r2))] ->
-		 Some t, Some (redexp_of_ast Evd.empty (Global.env()) (r1,r2))
+	     | [VARG_TACTIC_ARG (Redexp redexp)] ->
+		 None, Some redexp
+	     | [VARG_CONSTR t; VARG_TACTIC_ARG (Redexp redexp)] ->
+		 Some t, Some redexp
 	     | _ -> bad_vernac_args "DEFINITION"
 	   in 
 	   let stre,coe,objdef,idcoe = match kind with
@@ -807,9 +808,8 @@ let _ =
 let _ =
   add "Eval"
     (function
-       | VARG_TACTIC_ARG (Redexp (rn,unf)) :: VARG_CONSTR c :: g ->
+       | VARG_TACTIC_ARG (Redexp redexp) :: VARG_CONSTR c :: g ->
            let (evmap,sign) = get_evmap_sign (goal_of_args g) in
-           let redexp = redexp_of_ast evmap sign (rn,unf) in 
            let redfun = print_eval (reduction_of_redexp redexp) sign in 
 	   fun () -> mSG (redfun (judgment_of_com evmap sign c))
        | _ -> bad_vernac_args "Eval")
@@ -1196,20 +1196,19 @@ let _ =
        | _ -> bad_vernac_args "SYNTAX")
     
 let _ =
-  add "TacticDefinition"
-    (function 
-       | (VARG_IDENTIFIER na) :: (VARG_AST tacexp) :: idl ->
-	   let ids = 
-	     List.map 
-               (function
-                  | (VARG_IDENTIFIER id) -> (string_of_id id, Pcoq.ETast)
-                  | _ -> bad_vernac_args "TacticDefinition") 
-               idl
-	   in 
-	   fun () ->
-             let body = Ast.to_act_check_vars ids Pcoq.ETast tacexp in  
-	     Macros.add_macro_hint (string_of_id na) (List.map fst ids, body)
-       | _ -> bad_vernac_args "TacticDefinition")
+  add "TACDEF"
+    (let rec tacdef_fun lacc=function
+        (VARG_IDENTIFIER name)::(VARG_AST tacexp)::tl ->
+          let ve=
+            Tacinterp.val_interp (empty,empty_env,[],[],None) tacexp
+          in
+            tacdef_fun ((string_of_id name,ve)::lacc) tl
+       |[] ->
+         fun () ->
+           List.iter (fun (name,ve) -> Tacinterp.add_tacdef name ve) lacc
+       |_ -> bad_vernac_args "TACDEF"
+     in
+       tacdef_fun [])
 
 let _ =
   add "INFIX"
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 3329beff53..ea27b4aa67 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Names
 open Himsg
-open Proof_trees
+open Proof_type
 open Tacinterp
 open Coqast
 open Ast
@@ -95,7 +95,10 @@ let rec cvt_varg ast =
 
     | Node(_,"AST",[a]) -> VARG_AST a
     | Node(_,"ASTLIST",al) -> VARG_ASTLIST al
-    | Node(_,"TACTIC_ARG",[targ]) -> VARG_TACTIC_ARG (cvt_arg targ)
+    | Node(_,"TACTIC_ARG",[targ]) ->
+      let (evc,env)=Pfedit.get_evmap_sign None
+      in
+        VARG_TACTIC_ARG (interp_tacarg (evc,env,[],[],None) targ)
     | Node(_,"VERNACDYN",[Dynamic (_,d)]) -> VARG_DYN d
     | _ -> anomaly_loc (Ast.loc ast, "Vernacinterp.cvt_varg",
                         [< 'sTR "Unrecognizable ast node of vernac arg:";
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 8f10f8004c..0a5ccb9aac 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -3,7 +3,7 @@
 
 (*i*)
 open Names
-open Proof_trees
+open Proof_type
 (*i*)
 
 (* Interpretation of vernac phrases. *)