Ajout du langage de tactiques

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

9 files changed, 238 insertions, 159 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 533856fc12..4bef9a0eb9 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -250,9 +250,13 @@ let check_capture s ty = function
 	[< 'sTR ("The variable "^s^" occurs in its type") >]
   | _ -> ()
 
-let dbize k allow_soapp sigma =
+let dbize k sigma env allow_soapp lvar =
   let rec dbrec env = function
-    | Nvar(loc,s) -> fst (dbize_ref k sigma env loc s)
+    | Nvar(loc,s) ->
+      if List.mem s lvar then
+        RRef(loc,RVar (id_of_string s))
+      else
+        fst (dbize_ref k sigma env loc s)
 	  
    (*
    | Slam(_,ona,Node(_,"V$",l)) ->
@@ -306,8 +310,13 @@ let dbize k allow_soapp sigma =
     | Node(loc,"APPLISTEXPL", f::args) ->
 	RApp (loc,dbrec env f,List.map (dbrec env) args)
     | Node(loc,"APPLIST", Nvar(locs,s)::args) ->
-	let (c, impargs) = dbize_ref k sigma env locs s in
-	RApp (loc, c, dbize_args env impargs args)
+	let (c, impargs) =
+          if List.mem s lvar then
+            RRef(loc,RVar (id_of_string s)),[]
+          else
+            dbize_ref k sigma env locs s
+        in
+	  RApp (loc, c, dbize_args env impargs args)
     | Node(loc,"APPLIST", f::args) ->	   
 	RApp (loc,dbrec env f,List.map (dbrec env) args)
 	  
@@ -403,13 +412,28 @@ let dbize k allow_soapp sigma =
     aux 1 l args
 
   in 
-  dbrec
+  dbrec env
 
 (* constr_of_com takes an environment of typing assumptions,
  * and translates a command to a constr. *)
 
+(*Takes a list of variables which must not be globalized*)
+let interp_rawconstr_gen sigma env allow_soapp lvar com =
+  dbize CCI sigma (unitize_env (context env)) allow_soapp lvar com
+
 let interp_rawconstr sigma env com =
-  dbize CCI false sigma (unitize_env (context env)) com
+  interp_rawconstr_gen sigma env false [] com
+
+(*The same as interp_rawconstr but with a list of variables which must not be
+  globalized*)
+let interp_rawconstr_wo_glob sigma env lvar com =
+  dbize CCI sigma (unitize_env (context env)) false lvar com
+
+(*let raw_fconstr_of_com sigma env com =
+  dbize_fw sigma (unitize_env (context env)) [] com
+
+let raw_constr_of_compattern sigma env com = 
+  dbize_cci sigma (unitize_env env) com*)
 
 (* Globalization of AST quotations (mainly used in command quotations
    to get statically bound idents in grammar or pretty-printing rules) *)
@@ -501,14 +525,29 @@ let interp_constr_gen is_ass sigma env com =
 let interp_constr sigma env c = interp_constr_gen false sigma env c
 let interp_type sigma env   c = interp_constr_gen true sigma env c
 
-
 let judgment_of_com sigma env com = 
   let c = interp_rawconstr sigma env com in
   try
-    ise_resolve false sigma [] env c
+    ise_resolve false sigma [] env [] [] c
   with e -> 
     Stdpp.raise_with_loc (Ast.loc com) e
 
+(*To retype a list of key*constr with undefined key*)
+let retype_list sigma env lst=
+  List.map (fun (x,csr) -> (x,Retyping.mk_unsafe_judgment env sigma csr)) lst;;
+
+(*Interprets a constr according to two lists of instantiations (variables and
+  metas)*)
+let interp_constr1 sigma env lvar lmeta com =
+  let c =
+    interp_rawconstr_gen sigma env false (List.map (fun x -> string_of_id (fst
+      x)) lvar) com
+  and rtype=fun lst -> retype_list sigma env lst in
+  try
+    ise_resolve2 sigma env (rtype lvar) (rtype lmeta) c
+  with e -> 
+    Stdpp.raise_with_loc (Ast.loc com) e;;
+
 let typed_type_of_com sigma env com =
   let c = interp_rawconstr sigma env com in
   try 
@@ -521,6 +560,15 @@ let typed_type_of_com sigma env com =
 let interp_casted_constr sigma env com typ = 
   ise_resolve_casted sigma env typ (interp_rawconstr sigma env com)
 
+(*Interprets a casted constr according to two lists of instantiations
+  (variables and metas)*)
+let interp_casted_constr1 sigma env lvar lmeta com typ =
+  let c =
+    interp_rawconstr_gen sigma env false (List.map (fun x -> string_of_id (fst
+      x)) lvar) com
+  and rtype=fun lst -> retype_list sigma env lst in 
+  ise_resolve_casted_gen sigma env (rtype lvar) (rtype lmeta) typ c;;
+
 (*
 let dbize_fw  sigma env com = dbize FW sigma env com
 
@@ -619,101 +667,9 @@ let pattern_of_rawconstr c =
   (!metas,p)
 
 let interp_constrpattern sigma env com = 
-  let c = dbize CCI true sigma (unitize_env (context env)) com in
+  let c = dbize CCI sigma (unitize_env (context env)) true [] com in
   try 
     pattern_of_rawconstr c
   with e -> 
     Stdpp.raise_with_loc (Ast.loc com) e
 
-(* Translation of reduction expression: we need trad because of Fold
- * Moreover, reduction expressions are used both in tactics and in
- * vernac. *)
-
-open Closure
-open Tacred
-
-let glob_nvar com =
-  let s = nvar_of_ast com in
-  try 
-    Nametab.sp_of_id CCI (id_of_string s)
-  with Not_found -> 
-    error ("unbound variable "^s)
-
-let cvt_pattern sigma env = function
-  | Node(_,"PATTERN", Node(_,"COMMAND",[com])::nums) ->
-      let occs = List.map num_of_ast nums in
-      let c = interp_constr sigma env com in
-      let j = Typing.unsafe_machine env sigma c in
-      (occs, j.uj_val, j.uj_type)
-  | arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern")
-
-let cvt_unfold = function
-  | Node(_,"UNFOLD", com::nums) -> (List.map num_of_ast nums, glob_nvar com)
-  | arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold")
-
-let cvt_fold sigma sign = function
-  | Node(_,"COMMAND",[c]) -> interp_constr sigma sign c
-  | arg -> invalid_arg_loc (Ast.loc arg,"cvt_fold")
-
-let flag_of_ast lf =
-  let beta = ref false in
-  let delta = ref false in
-  let iota = ref false in
-  let idents = ref (None: (sorts oper -> bool) option) in
-  let set_flag = function
-    | Node(_,"Beta",[]) -> beta := true
-    | Node(_,"Delta",[]) -> delta := true
-    | Node(_,"Iota",[]) -> iota := true
-    | Node(loc,"Unf",l) ->
-        if !delta then
-          if !idents = None then
-            let idl = List.map glob_nvar l in
-            idents := Some
-              (function
-                 | Const sp -> List.mem sp idl
-                 | Abst sp -> List.mem sp idl
-                 | _ -> false)
-          else 
-	    user_err_loc
-	      (loc,"flag_of_ast",
-	       [< 'sTR"Cannot specify identifiers to unfold twice" >])
-        else 
-	  user_err_loc(loc,"flag_of_ast",
-                       [< 'sTR"Delta must be specified before" >])
-    | Node(loc,"UnfBut",l) ->
-        if !delta then
-          if !idents = None then
-            let idl = List.map glob_nvar l in
-            idents := Some
-              (function
-                 | Const sp -> not (List.mem sp idl)
-                 | Abst sp -> not (List.mem sp idl)
-                 | _ -> false)
-          else 
-	    user_err_loc
-	      (loc,"flag_of_ast",
-	       [< 'sTR"Cannot specify identifiers to unfold twice" >])
-        else 
-	  user_err_loc(loc,"flag_of_ast",
-                       [< 'sTR"Delta must be specified before" >])
-    | arg -> invalid_arg_loc (Ast.loc arg,"flag_of_ast")
-  in
-  List.iter set_flag lf;
-  { r_beta = !beta;
-    r_iota = !iota;
-    r_delta = match (!delta,!idents) with
-      | (false,_) -> (fun _ -> false)
-      | (true,None) -> (fun _ -> true)
-      | (true,Some p) -> p }
-
-let redexp_of_ast sigma sign = function
-  | ("Red", []) -> Red
-  | ("Hnf", []) -> Hnf
-  | ("Simpl", []) -> Simpl
-  | ("Unfold", ul) -> Unfold (List.map cvt_unfold ul)
-  | ("Fold", cl) -> Fold (List.map (cvt_fold sigma sign) cl)
-  | ("Cbv",lf) -> Cbv(UNIFORM, flag_of_ast lf)
-  | ("Lazy",lf) -> Lazy(UNIFORM, flag_of_ast lf)
-  | ("Pattern",lp) -> Pattern (List.map (cvt_pattern sigma sign) lp)
-  | (s,_) -> invalid_arg ("malformed reduction-expression: "^s)
-
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 1383dc655f..46c8f5b665 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -20,12 +20,21 @@ val interp_type          : 'a evar_map -> env -> Coqast.t -> constr
 val typed_type_of_com    : 'a evar_map -> env -> Coqast.t -> typed_type
 val judgment_of_com      : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
 
+(*Interprets a constr according to two lists of instantiations (variables and
+  metas)*)
+val interp_constr1     :
+  'a evar_map -> env -> (identifier * constr) list ->
+    (int * constr) list -> Coqast.t -> constr
+
+(*Interprets a casted constr according to two lists of instantiations
+  (variables and metas)*)
+val interp_casted_constr1 :
+  'a evar_map -> env -> (identifier * constr) list ->
+    (int * constr) list -> Coqast.t -> constr -> constr
+
 val interp_constrpattern : 
   'a evar_map -> env -> Coqast.t -> int list * constr_pattern
 
-val redexp_of_ast : 
-  'a evar_map -> env -> string * Coqast.t list -> Tacred.red_expr
-
 (* Translation rules from V6 to V7:
 
 constr_of_com_casted -> interp_casted_constr
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index dec8594750..41f0a82d4b 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -42,7 +42,7 @@ GEXTEND Gram
     [ [ c = Constr.sort -> <:ast< (CONSTR $c) >> ] ]
   ;
   tacarg:
-    [ [ tcl = Tactic.tactic_com_list -> tcl ] ]
+    [ [ tcl = Tactic.tactic -> tcl ] ]
   ;
 END;
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 4ab8b33ac2..96be64616d 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -16,7 +16,9 @@ GEXTEND Gram
     [ [ c = Prim.ast -> c ] ]
   ;
   constr:
-    [ [ c = constr8 -> c ] ]
+    [ [ c = constr8 -> c 
+      | IDENT "Eval"; rtc=Tactic.red_tactic; "in"; c=constr8 ->
+        <:ast<(EVAL $c (REDEXP $rtc))>> ] ]
   ;
   lconstr:
     [ [ c = constr10 -> c ] ]
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index f19e373733..9a64fd03c1 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -16,9 +16,15 @@ GEXTEND Gram
   identarg:
     [ [ id = IDENT -> <:ast< ($VAR $id) >> ] ]
   ;
+  pure_numarg:
+     [ [ n = Prim.number -> n
+       | "-"; n = Prim.number -> Coqast.Num (Ast.loc n, ( - Ast.num_of_ast n))
+     ] ]
+  ;
   numarg:
     [ [ n = Prim.number -> n
       | "-"; n = Prim.number -> Coqast.Num (Ast.loc n, ( - Ast.num_of_ast n))
+      |	id = identarg -> id
       ] ]
   ;
   constrarg:
@@ -27,6 +33,9 @@ GEXTEND Gram
   lconstrarg:
     [ [ c = Constr.lconstr -> <:ast< (COMMAND $c) >> ] ]
   ;
+  castedconstrarg:
+    [ [ c = Constr.constr -> <:ast< (CASTEDCOMMAND $c) >> ] ]
+  ;
   ne_identarg_list:
     [ [ l = LIST1 identarg -> l ] ]
   ;
@@ -34,15 +43,18 @@ GEXTEND Gram
     [ [ n = numarg; l = ne_num_list -> n :: l | n = numarg -> [n] ] ]
   ;
   pattern_occ:
-    [ [ nl = ne_num_list; c = constrarg -> <:ast< (PATTERN $c ($LIST $nl)) >>
+    [ [ nl = LIST1 pure_numarg; c = constrarg ->
+         <:ast< (PATTERN $c ($LIST $nl)) >>
       | c = constrarg -> <:ast< (PATTERN $c) >> ] ]
   ;
   ne_pattern_list:
     [ [ l = LIST1 pattern_occ -> l ] ]
   ;
   pattern_occ_hyp:
-    [ [ nl = ne_num_list; IDENT "Goal" -> <:ast<(CCLPATTERN ($LIST $nl))>>
-      | nl = ne_num_list; id = identarg -> <:ast<(HYPPATTERN $id ($LIST $nl))>>
+    [ [ nl = LIST1 pure_numarg; IDENT "Goal" ->
+          <:ast<(CCLPATTERN ($LIST $nl))>>
+      | nl = LIST1 pure_numarg; id = identarg ->
+          <:ast<(HYPPATTERN $id ($LIST $nl))>>
       | IDENT "Goal" -> <:ast< (CCLPATTERN) >>
       | id = identarg -> <:ast< (HYPPATTERN $id) >> ] ]
   ;
@@ -53,8 +65,8 @@ GEXTEND Gram
     [ [ p= ne_intropattern ->  <:ast< (INTROPATTERN $p)>> ]]
   ;
   ne_intropattern:
-    [ [   tc = LIST1 simple_intropattern -> 
-           <:ast< (LISTPATTERN ($LIST $tc))>> ] ]
+    [ [ tc = LIST1 simple_intropattern -> 
+          <:ast< (LISTPATTERN ($LIST $tc))>> ] ]
   ;
   simple_intropattern:
     [ [ "["; tc = LIST1 intropattern  SEP "|" ; "]" -> 
@@ -86,7 +98,7 @@ GEXTEND Gram
             | Coqast.Node(_,"COMMAND",[c]) -> coerce_to_var "c1" c
             | _ -> assert false
           in <:ast<(BINDINGS (BINDING ($VAR $id) $c2) ($LIST $bl))>>
-      | n = numarg; ":="; c = constrarg; bl = simple_binding_list ->
+      | n = pure_numarg; ":="; c = constrarg; bl = simple_binding_list ->
           <:ast<(BINDINGS (BINDING $n $c) ($LIST $bl))>>
       | c1 = constrarg; bl = com_binding_list ->
           <:ast<(BINDINGS (BINDING $c1) ($LIST $bl))>>
@@ -105,7 +117,8 @@ GEXTEND Gram
     [ [ c = constrarg; l = constrarg_list -> c :: l | -> [] ] ]
   ;
   unfold_occ:
-    [ [ nl = ne_num_list; c = identarg -> <:ast< (UNFOLD $c ($LIST $nl)) >>
+    [ [ nl = LIST1 pure_numarg; c = identarg ->
+         <:ast< (UNFOLD $c ($LIST $nl)) >>
       | c = identarg -> <:ast< (UNFOLD $c) >> ] ]
   ;
   ne_unfold_occ_list:
@@ -169,20 +182,83 @@ GEXTEND Gram
 (* Tactics grammar rules *)
 
 GEXTEND Gram
-  tactic_com_list:
-    [ [ y = tactic_com; ";"; l = LIST1 tactic_com_tail SEP ";" ->
-          <:ast< (TACTICLIST $y ($LIST $l)) >>
-      | y = tactic_com -> <:ast< (TACTICLIST $y) >> ] ]
-  ;
-  tactic_com_tail:
-    [ [ t1 = tactic_com -> t1
-      | "["; l = LIST0 tactic_com_list SEP "|"; "]" ->
-          <:ast< (TACLIST ($LIST $l)) >> ] ]
-  ;
-  tactic_com:
-    [ [ st = simple_tactic; "Orelse"; tc = tactic_com ->
-          <:ast< (ORELSE $st $tc) >>
-      | st = simple_tactic -> st ] ]
+  input_fun:
+    [ [ l = identarg -> l
+      | "()" -> <:ast< (VOID) >> ] ]
+  ;
+  let_clause:
+    [ [ id = identarg; "="; te=tactic_expr -> <:ast< (LETCLAUSE $id $te) >> ] ]
+  ;
+  rec_clause:
+    [ [ name = identarg; it = LIST1 input_fun; "->"; body = tactic_expr ->
+          <:ast< (RECCLAUSE $name (FUNVAR ($LIST $it)) $body) >> ] ]
+  ;
+  match_hyps:
+    [ [ id = identarg; ":"; pc = constrarg ->
+          <:ast< (MATCHCONTEXTHYPS $id $pc) >>
+      | IDENT "_"; ":"; pc = constrarg -> <:ast< (MATCHCONTEXTHYPS $pc) >> ] ]
+  ;
+  match_context_rule:
+    [ [ "["; largs = LIST0 match_hyps SEP ";"; "|-"; pc = constrarg; "]"; "->";
+          te = tactic_expr ->
+            <:ast< (MATCHCONTEXTRULE ($LIST $largs) $pc $te) >> 
+      | IDENT "_"; "->"; te = tactic_expr -> <:ast< (MATCHCONTEXTRULE $te) >>
+    ] ]
+  ;
+  match_rule:
+    [ [ "["; com = constrarg; "]"; "->"; te = tactic_expr ->
+          <:ast<(MATCHRULE $com $te)>>
+      | IDENT "_"; "->"; te = tactic_expr -> <:ast< (MATCHRULE $te) >> ] ]
+  ;
+  tactic_expr:
+    [ [ ta0 = tactic_expr; ";"; ta1 = tactic_expr ->
+         <:ast< (TACTICLIST $ta0 $ta1) >>
+      | ta = tactic_expr; ";"; "["; lta = LIST0 tactic_expr SEP "|"; "]" ->
+         <:ast< (TACTICLIST $ta (TACLIST ($LIST $lta))) >>
+      | y = tactic_atom -> y ] ]
+  ;
+  tactic_atom:
+    [ [ IDENT "Fun"; it = LIST1 input_fun ; "->"; body = tactic_expr ->
+          <:ast< (FUN (FUNVAR ($LIST $it)) $body) >>
+      | IDENT "Rec"; rc = rec_clause -> <:ast< (REC $rc) >>
+      |	IDENT "Rec"; rc = rec_clause; IDENT "In"; body = tactic_expr ->
+          <:ast< (REC (RECDECL $rc) $body) >>
+      | IDENT "Rec"; rc = rec_clause; IDENT "And";
+          rcl = LIST1 rec_clause SEP IDENT "And"; IDENT "In";
+          body = tactic_expr ->
+            <:ast< (REC (RECDECL $rc ($LIST $rcl)) $body) >>
+      | IDENT "Let"; llc = LIST1 let_clause SEP IDENT "And"; IDENT "In";
+          u = tactic_expr -> <:ast< (LET (LETDECL ($LIST $llc)) $u) >>
+      |	IDENT "Match"; IDENT "Context"; IDENT "With";
+          mrl = LIST1 match_context_rule SEP "|" ->
+            <:ast< (MATCHCONTEXT ($LIST $mrl)) >>
+      |	IDENT "Match"; com = constrarg; IDENT "With";
+          mrl = LIST1 match_rule SEP "|" -> <:ast< (MATCH $com ($LIST $mrl)) >>
+      |	"'("; te = tactic_expr; ")" -> te
+      |	"'("; te = tactic_expr; tel=LIST1 tactic_expr; ")" ->
+          <:ast< (APP $te ($LIST tel)) >>
+      | IDENT "First" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+          <:ast<(FIRST ($LIST $l))>>
+      | IDENT "Info"; tc = tactic_expr -> <:ast< (INFO $tc) >>
+      |	IDENT "Solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
+          <:ast<(TCLSOLVE ($LIST $l))>>
+      |	IDENT "Try"; ta = tactic_atom -> <:ast< (TRY $ta) >>
+      | IDENT "Do"; n = numarg; ta = tactic_atom -> <:ast< (DO $n $ta) >>
+      | IDENT "Repeat"; ta = tactic_atom -> <:ast< (REPEAT $ta) >>
+      |	IDENT "Idtac" -> <:ast< (IDTAC) >>
+      |	IDENT "Fail" -> <:ast<(FAIL)>>
+      |	ta0 = tactic_atom; "Orelse"; ta1 = tactic_atom ->
+          <:ast< (ORELSE $ta0 $ta1) >>
+      |	st = simple_tactic -> st
+      |	tca = tactic_arg -> tca ] ]
+  ;
+  tactic_arg:
+    [ [ "()" -> <:ast< (VOID) >>
+      | n = pure_numarg -> n
+      |	c=constrarg -> 
+          (match c with
+            Coqast.Node(_,"COMMAND",[Coqast.Nvar(_,s)]) -> <:ast<($VAR $s)>>
+           |_ -> c) ] ]
   ;
   simple_tactic:
     [ [ IDENT "Fix"; n = numarg -> <:ast< (Fix $n) >>
@@ -224,8 +300,9 @@ GEXTEND Gram
                    <:ast< (SuperAuto $a0 $a1 $a2 $a3) >>
       | IDENT "Auto"; n = numarg; IDENT "Decomp" -> <:ast< (DAuto $n) >>
       | IDENT "Auto"; IDENT "Decomp" -> <:ast< (DAuto) >>
-      | IDENT "Auto"; n = numarg; IDENT "Decomp"; p = numarg-> <:ast< (DAuto $n $p) >>
-      ]];
+      | IDENT "Auto"; n = numarg; IDENT "Decomp"; p = numarg ->
+          <:ast< (DAuto $n $p) >>
+      ] ];
     END
 
 GEXTEND Gram
@@ -250,7 +327,7 @@ GEXTEND Gram
           <:ast< (Elim ($LIST $cl)) >>
       | IDENT "Assumption" -> <:ast< (Assumption) >>
       | IDENT "Contradiction" -> <:ast< (Contradiction) >>
-      | IDENT "Exact"; c = constrarg -> <:ast< (Exact $c) >>
+      | IDENT "Exact"; c = castedconstrarg -> <:ast< (Exact $c) >>
       | IDENT "OldElim"; c = constrarg -> <:ast< (OldElim $c) >>
       | IDENT "ElimType"; c = constrarg -> <:ast< (ElimType $c) >>
       | IDENT "Case"; cl = constrarg_binding_list ->
@@ -264,10 +341,6 @@ GEXTEND Gram
              <:ast< (DecomposeOr $c) >>
       | IDENT "Decompose"; "["; l = ne_identarg_list; "]"; c = constrarg ->
           <:ast< (DecomposeThese (CLAUSE ($LIST $l)) $c) >>
-      |	IDENT "First" ; "["; l = LIST0 tactic_com_list SEP "|"; "]" ->
-          <:ast<(FIRST ($LIST $l))>>
-      |	IDENT "Solve" ; "["; l = LIST0 tactic_com_list SEP "|"; "]" ->
-          <:ast<(TCLSOLVE ($LIST $l))>>
       | IDENT "Cut"; c = constrarg -> <:ast< (Cut $c) >>
       | IDENT "Specialize"; n = numarg; lcb = constrarg_binding_list ->
           <:ast< (Specialize $n ($LIST $lcb))>>
@@ -285,13 +358,11 @@ GEXTEND Gram
                 <:ast< (Clear (CLAUSE ($LIST $l))) >>
       | IDENT "Move"; id1 = identarg; IDENT "after"; id2 = identarg -> 
                 <:ast< (MoveDep $id1 $id2) >>
-      | IDENT "Do"; n = numarg; tc = tactic_com -> <:ast< (DO $n $tc) >>
-      | IDENT "Try"; tc = tactic_com -> <:ast< (TRY $tc) >>
-      | IDENT "Info"; tc = tactic_com -> <:ast< (INFO $tc) >>
-      | IDENT "Repeat"; tc = tactic_com -> <:ast< (REPEAT $tc) >>
-      | IDENT "Abstract"; tc = tactic_com -> <:ast< (ABSTRACT (TACTIC $tc)) >>
-      | IDENT "Abstract"; tc = tactic_com; "using";  s=identarg 
-                                   -> <:ast< (ABSTRACT $s (TACTIC $tc)) >>
+(*To do: put Abstract in Refiner*)
+      | IDENT "Abstract"; tc = tactic_expr -> <:ast< (ABSTRACT (TACTIC $tc)) >>
+      | IDENT "Abstract"; tc = tactic_expr; "using";  s=identarg ->
+          <:ast< (ABSTRACT $s (TACTIC $tc)) >>
+(*End of To do*)
       | IDENT "Left"; bl = with_binding_list -> <:ast< (Left $bl) >>
       | IDENT "Right"; bl = with_binding_list -> <:ast< (Right $bl) >>
       | IDENT "Split"; bl = with_binding_list -> <:ast< (Split $bl) >>
@@ -305,23 +376,22 @@ GEXTEND Gram
       | IDENT "Absurd"; c = constrarg -> <:ast< (Absurd $c) >>
       | IDENT "Idtac" -> <:ast< (Idtac) >>
       | IDENT "Fail" -> <:ast< (Fail) >>
-      | "("; tcl = tactic_com_list; ")" -> tcl
       | r = red_tactic; cl = clausearg -> <:ast< (Reduce (REDEXP $r) $cl) >>
       (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
       | IDENT "Change"; c = constrarg; cl = clausearg ->
 	  <:ast< (Change $c $cl) >> 
       | IDENT "ML"; s = Prim.string -> <:ast< (MLTACTIC $s) >> ]
 
-    | [ id = identarg; l = constrarg_list ->
+(*    | [ id = identarg; l = constrarg_list ->
           match (isMeta (nvar_of_ast id), l) with
             | (true, []) -> id
             | (false, _) -> <:ast< (CALL $id ($LIST $l)) >>
             | _ -> Util.user_err_loc
                   (loc, "G_tactic.meta_tactic",
                    [< 'sTR"Cannot apply arguments to a meta-tactic." >])
-      ] ]
+      ] *)]
   ;
   tactic:
-    [ [ tac = tactic_com_list -> tac ] ]
+    [ [ tac = tactic_expr -> tac ] ]
   ;
 END
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 25010016ca..bea4c46aa5 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -2,7 +2,9 @@
 (* $Id$ *)
 
 open Pcoq
-
+open Pp
+open Tactic
+open Util
 open Vernac
 
 GEXTEND Gram
@@ -121,7 +123,8 @@ GEXTEND Gram
       [ [ IDENT "Abstraction"; id = identarg; "["; l = ne_numarg_list; "]";
         ":="; c = constrarg; "." ->
           <:ast< (ABSTRACTION $id $c ($LIST $l)) >>
-      ] ];
+      ] ]
+  ;
   END
 
 (* Gallina inductive declarations *)
@@ -425,6 +428,10 @@ GEXTEND Gram
   [ [ -> []
     | ":"; l = LIST1 identarg -> l ] ]
   ;
+  vrec_clause:
+    [ [ name=identarg; it=LIST1 input_fun; ":="; body=tactic_expr ->
+          <:ast<(RECCLAUSE $name (FUNVAR ($LIST $it)) $body)>> ] ]
+  ;
   command:
     [ [ IDENT "Goal"; c = constrarg; "." -> <:ast< (GOAL $c) >>
       | IDENT "Goal"; "." -> <:ast< (GOAL) >>
@@ -481,11 +488,29 @@ GEXTEND Gram
 
 (* Tactic Definition *)
 
-      | IDENT "Tactic"; "Definition"; id = identarg; "[";
-        ids = ne_identarg_list; "]"; ":="; tac = Prim.astact; "." ->
-          <:ast< (TacticDefinition $id (AST $tac) ($LIST $ids)) >>
-      | IDENT "Tactic"; "Definition"; id = identarg; ":="; tac = Prim.astact;
-        "." -> <:ast< (TacticDefinition $id (AST $tac)) >>
+      |IDENT "Tactic"; "Definition"; name=identarg; ":="; body=Tactic.tactic;
+        "." -> <:ast<(TACDEF $name (AST $body))>>
+      |IDENT "Tactic"; "Definition"; name=identarg; largs=LIST1 input_fun;
+        ":="; body=Tactic.tactic; "." ->
+        <:ast<(TACDEF $name (AST (FUN (FUNVAR ($LIST $largs)) $body)))>>
+      |IDENT "Recursive"; IDENT "Tactic"; "Definition"; vc=vrec_clause ; "." ->
+        (match vc with
+            Coqast.Node(_,"RECCLAUSE",nme::tl) ->
+              <:ast<(TACDEF $nme (AST (REC $vc)))>>
+           |_ ->
+             anomalylabstrm "Gram.vernac" [<'sTR "Not a correct RECCLAUSE">])
+      |IDENT "Recursive"; IDENT "Tactic"; "Definition"; vc=vrec_clause;
+        IDENT "And"; vcl=LIST1 vrec_clause SEP IDENT "And"; "." ->
+        let nvcl=
+          List.fold_right
+            (fun e b -> match e with
+                Coqast.Node(_,"RECCLAUSE",nme::_) ->
+                  nme::<:ast<(AST (REC $e))>>::b
+               |_ ->
+                 anomalylabstrm "Gram.vernac" [<'sTR
+                   "Not a correct RECCLAUSE">]) (vc::vcl) []
+        in
+          <:ast<(TACDEF ($LIST $nvcl))>>
 
 (* Hints for Auto and EAuto *)
 
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index 847b9a8fae..dca9a2fdd7 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -135,7 +135,8 @@ rule token = parse
 	if is_keyword s then ("",s) else ("IDENT",s) }
   | decimal_literal | hex_literal | oct_literal | bin_literal
       { ("INT", Lexing.lexeme lexbuf) }
-  | "(" | ")" | "[" | "]" | "{" | "}" | "." | "_" | ";" | "`" | "->"
+  | "(" | ")" | "[" | "]" | "{" | "}" | "." | "_" | ";"| "`" | "()" | "'("
+  | "->"
       { ("", Lexing.lexeme lexbuf) }
   | symbolchar+
       { ("", Lexing.lexeme lexbuf) }
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 418188be5f..f0b13f23e6 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -272,6 +272,7 @@ module Tactic =
       Hashtbl.add utactic s (ListAst e); e
     
     let binding_list = gec "binding_list"
+    let castedconstrarg = gec "castedconstrarg"
     let com_binding_list = gec_list "com_binding_list"
     let constrarg = gec "constrarg"
     let constrarg_binding_list = gec_list "constrarg_binding_list"
@@ -279,8 +280,13 @@ module Tactic =
     let lconstrarg_binding_list = gec_list "lconstrarg_binding_list"
     let constrarg_list = gec_list "constrarg_list"
     let identarg = gec "identarg"
+    let input_fun = gec "input_fun"
     let lconstrarg = gec "lconstrarg"
+    let let_clause = gec "let_clause"
     let clausearg = gec "clausearg"
+    let match_context_rule = gec "match_context_rule"
+    let match_hyps = gec "match_hyps"
+    let match_rule = gec "match_rule"
     let ne_identarg_list = gec_list "ne_identarg_list"
     let ne_num_list = gec_list "ne_num_list"
     let ne_pattern_list = gec_list "ne_pattern_list"
@@ -290,6 +296,7 @@ module Tactic =
     let ne_intropattern = gec "ne_intropattern"
     let simple_intropattern = gec "simple_intropattern"
     let ne_unfold_occ_list = gec_list "ne_unfold_occ_list"
+    let rec_clause = gec "rec_clause"
     let red_tactic = gec "red_tactic"
     let red_flag = gec "red_flag"
     let autoarg_depth = gec "autoarg_depth"
@@ -300,13 +307,14 @@ module Tactic =
     let numarg = gec "numarg"
     let pattern_occ = gec "pattern_occ"
     let pattern_occ_hyp = gec "pattern_occ_hyp"
+    let pure_numarg = gec "pure_numarg"
     let simple_binding = gec "simple_binding"
     let simple_binding_list = gec_list "simple_binding_list"
     let simple_tactic = gec "simple_tactic"
     let tactic = gec "tactic"
-    let tactic_com = gec "tactic_com"
-    let tactic_com_list = gec "tactic_com_list"
-    let tactic_com_tail = gec "tactic_com_tail"
+    let tactic_arg = gec "tactic_arg"
+    let tactic_atom = gec "tactic_atom"
+    let tactic_expr = gec "tactic_expr"
     let unfold_occ = gec "unfold_occ"
     let with_binding_list = gec "with_binding_list"
     let fixdecl = gec_list "fixdecl"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d7313e296c..a60bfec5e8 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -91,6 +91,7 @@ module Tactic :
     val autoarg_excluding : Coqast.t Gram.Entry.e
     val autoarg_usingTDB : Coqast.t Gram.Entry.e
     val binding_list : Coqast.t Gram.Entry.e
+    val castedconstrarg : Coqast.t Gram.Entry.e
     val clausearg : Coqast.t Gram.Entry.e
     val cofixdecl : Coqast.t list Gram.Entry.e
     val com_binding_list : Coqast.t list Gram.Entry.e
@@ -99,9 +100,14 @@ module Tactic :
     val constrarg_list : Coqast.t list Gram.Entry.e
     val fixdecl : Coqast.t list Gram.Entry.e
     val identarg : Coqast.t Gram.Entry.e
+    val input_fun : Coqast.t Gram.Entry.e
     val intropattern : Coqast.t Gram.Entry.e
     val lconstrarg : Coqast.t Gram.Entry.e
     val lconstrarg_binding_list : Coqast.t list Gram.Entry.e
+    val let_clause : Coqast.t Gram.Entry.e
+    val match_context_rule : Coqast.t Gram.Entry.e
+    val match_hyps : Coqast.t Gram.Entry.e
+    val match_rule : Coqast.t Gram.Entry.e
     val ne_identarg_list : Coqast.t list Gram.Entry.e
     val ne_intropattern : Coqast.t Gram.Entry.e
     val ne_num_list : Coqast.t list Gram.Entry.e
@@ -113,6 +119,8 @@ module Tactic :
     val one_intropattern : Coqast.t Gram.Entry.e
     val pattern_occ : Coqast.t Gram.Entry.e
     val pattern_occ_hyp : Coqast.t Gram.Entry.e
+    val pure_numarg : Coqast.t Gram.Entry.e
+    val rec_clause : Coqast.t Gram.Entry.e
     val red_flag : Coqast.t Gram.Entry.e
     val red_tactic : Coqast.t Gram.Entry.e
     val simple_binding : Coqast.t Gram.Entry.e
@@ -120,10 +128,10 @@ module Tactic :
     val simple_intropattern : Coqast.t Gram.Entry.e
     val simple_tactic : Coqast.t Gram.Entry.e
     val tactic : Coqast.t Gram.Entry.e
-    val tactic_com : Coqast.t Gram.Entry.e
-    val tactic_com_list : Coqast.t Gram.Entry.e
-    val tactic_com_tail : Coqast.t Gram.Entry.e
+    val tactic_arg : Coqast.t Gram.Entry.e
+    val tactic_atom : Coqast.t Gram.Entry.e
     val tactic_eoi : Coqast.t Gram.Entry.e
+    val tactic_expr : Coqast.t Gram.Entry.e
     val unfold_occ : Coqast.t Gram.Entry.e
     val with_binding_list : Coqast.t Gram.Entry.e
   end