Réorganisation des tclTHEN (cf dev/changements.txt)

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

8 files changed, 323 insertions, 259 deletions

diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 7c5152672..0c916495a 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -23,9 +23,11 @@ open Tacred
 open Typing
 open Nametab
 
+(*
 let is_bind = function
-  | Bindings _ -> true
+  | Tacexpr.Cbindings _ -> true
   | _ -> false
+*)
 
 (* Functions on goals *)
 
@@ -48,10 +50,9 @@ let children_of_proof pf =
 				    
 let goal_of_proof pf = pf.goal
 
-let subproof_of_proof pf =
-  match pf.subproof with
-    | None -> failwith "subproof_of_proof"
-    | Some pf -> pf
+let subproof_of_proof pf = match pf.ref with
+  | Some (Tactic (_,pf), _) -> pf
+  | _ -> failwith "subproof_of_proof"
 
 let status_of_proof pf = pf.status
 
@@ -59,7 +60,9 @@ let is_complete_proof pf = pf.status = Complete_proof
 
 let is_leaf_proof pf = (pf.ref = None)
 
-let is_tactic_proof pf = (pf.subproof <> None)
+let is_tactic_proof pf = match pf.ref with
+  | Some (Tactic _, _) -> true
+  | _ -> false
 
 
 (*******************************************************************)
@@ -245,21 +248,24 @@ let pr_subgoals_existential sigma = function
       v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () 
 	   ++ pg1 ++ prest ++ fnl ())
 
+(*
 open Ast
 open Termast
+open Tacexpr
+open Rawterm
 
 let ast_of_cvt_bind f = function
-  | (NoDep n,c) -> ope ("BINDING", [(num n); ope ("COMMAND",[(f c)])])
-  | (Dep  id,c) -> ope ("BINDING", [nvar id; ope  ("COMMAND",[(f c)])]) 
-  | (Com,c)     -> ope ("BINDING", [ope ("COMMAND",[(f c)])])
+  | (NoDepBinding n,c) -> ope ("BINDING", [(num n); ope ("CONSTR",[(f c)])])
+  | (DepBinding  id,c) -> ope ("BINDING", [nvar id; ope  ("CONSTR",[(f c)])]) 
+  | (AnonymousBinding,c) -> ope ("BINDING", [ope ("CONSTR",[(f c)])])
 
 let rec ast_of_cvt_intro_pattern = function
   | WildPat   -> ope ("WILDCAR",[])
   | IdPat id  -> nvar id
-  | DisjPat l -> ope ("DISJPATTERN",  (List.map ast_of_cvt_intro_pattern l))
+(*  | DisjPat l -> ope ("DISJPATTERN",  (List.map ast_of_cvt_intro_pattern l))*)
   | ConjPat l -> ope ("CONJPATTERN",  (List.map ast_of_cvt_intro_pattern l))
-  | ListPat l -> ope ("LISTPATTERN",  (List.map ast_of_cvt_intro_pattern l))
-
+*)
+(*
 (* Gives the ast list corresponding to a reduction flag *)
 open RedFlags
 
@@ -280,14 +286,19 @@ let last_of_cvt_flags red =
    else [ope("Delta",[]);ope("Unf",lqid)])@
   (if (red_set red fIOTA) then [ope("Iota",[])]
    else [])
-
+*)
+(*
 (* Gives the ast corresponding to a reduction expression *)
+open Rawterm
+
 let ast_of_cvt_redexp = function
   | Red _ -> ope ("Red",[])
   | Hnf -> ope("Hnf",[])
   | Simpl -> ope("Simpl",[])
+(*
   | Cbv flg -> ope("Cbv",last_of_cvt_flags flg)
   | Lazy flg -> ope("Lazy",last_of_cvt_flags flg)
+*)
   | Unfold l ->
     ope("Unfold",List.map (fun (locc,sp) -> ope("UNFOLD",
       [match sp with
@@ -297,24 +308,27 @@ let ast_of_cvt_redexp = function
 	      (shortest_qualid_of_global (Global.env()) (ConstRef sp))]
       @(List.map num locc))) l)
   | Fold l ->
-    ope("Fold",List.map (fun c -> ope ("COMMAND",
+    ope("Fold",List.map (fun c -> ope ("CONSTR",
       [ast_of_constr false (Global.env ()) c])) l)
   | Pattern l ->
-    ope("Pattern",List.map (fun (locc,csr,_) -> ope("PATTERN",
-      [ope ("COMMAND",[ast_of_constr false (Global.env ()) csr])]@
+    ope("Pattern",List.map (fun (locc,csr) -> ope("PATTERN",
+      [ope ("CONSTR",[ast_of_constr false (Global.env ()) csr])]@
       (List.map num locc))) l)
-
+*)
 (* Gives the ast corresponding to a tactic argument *)
+(*
 let ast_of_cvt_arg = function
   | Identifier id   -> nvar id
+(*
   | Qualid qid      -> ast_of_qualid qid
+*)
   | Quoted_string s -> string s
   | Integer n       -> num n 
-  | Command c       -> ope ("COMMAND",[c])
+(*  | Command c       -> ope ("CONSTR",[c])*)
   | Constr  c       -> 
-    ope ("COMMAND",[ast_of_constr false (Global.env ()) c])
+    ope ("CONSTR",[ast_of_constr false (Global.env ()) c])
   | OpenConstr  (_,c)       -> 
-    ope ("COMMAND",[ast_of_constr false (Global.env ()) c])
+    ope ("CONSTR",[ast_of_constr false (Global.env ()) c])
   | Constr_context _ ->
     anomalylabstrm "ast_of_cvt_arg" (str
       "Constr_context argument could not be used")
@@ -323,6 +337,7 @@ let ast_of_cvt_arg = function
 	| InHyp id -> ope ("INHYP", [nvar id])
 	| InHypType id -> ope ("INHYPTYPE", [nvar id]) in
       ope ("CLAUSE", List.map transl idl)
+(*
   | Bindings bl     -> ope ("BINDINGS", 
 			    List.map (ast_of_cvt_bind (fun x -> x)) bl)
   | Cbindings bl    -> 
@@ -330,12 +345,15 @@ let ast_of_cvt_arg = function
 	   List.map 
 	     (ast_of_cvt_bind
 		(ast_of_constr false (Global.env ()))) bl)
+*)
+(* TODO
   | Tacexp ast      -> ope ("TACTIC",[ast])
   | Tac (tac,ast) -> ast
+*)
   | Redexp red -> ope("REDEXP",[ast_of_cvt_redexp red])
-  | Fixexp (id,n,c) -> ope ("FIXEXP",[nvar id; num n; ope ("COMMAND",[c])])
-  | Cofixexp (id,c) -> ope ("COFIXEXP",[nvar id; ope ("COMMAND",[c])])
-  | Intropattern p ->  ast_of_cvt_intro_pattern p
+  | Fixexp (id,n,c) -> ope ("FIXEXP",[nvar id; num n; ope ("CONSTR",[ast_of_constr false (Global.env ()) c])])
+  | Cofixexp (id,c) -> ope ("COFIXEXP",[nvar id; ope ("CONSTR",[ast_of_constr false (Global.env ()) c])])
+(*  | Intropattern p ->  ast_of_cvt_intro_pattern p*)
   | Letpatterns (gl_occ_opt,hyp_occ_list) ->
      let hyps_pats =
        List.map
@@ -347,4 +365,4 @@ let ast_of_cvt_arg = function
 	 | None -> hyps_pats
 	 | Some l -> hyps_pats @ [ope ("CCLPATTERN", List.map num l)] in
      ope ("LETPATTERNS", all_pats)
-
+*)
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index d6a1a51d5..889c16aba 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -67,4 +67,6 @@ val pr_evars_int : int -> (int * goal) list -> std_ppcmds
 val pr_subgoals_existential : evar_map -> goal list -> std_ppcmds
 
 (* Gives the ast corresponding to a tactic argument *)
+(*
 val ast_of_cvt_arg : tactic_arg ->  Coqast.t 
+*)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index afee5e2a9..c9f8aca31 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -5,32 +5,27 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
+
+(*i $Id$ *)
+
 (*i*)
 open Environ
 open Evd
 open Names
 open Term
 open Util
+open Tacexpr
+open Rawterm
+open Genarg
 (*i*)
 
 (* This module defines the structure of proof tree and the tactic type. So, it
    is used by Proof_tree and Refiner *)
 
-type bindOcc = 
-  | Dep of identifier
-  | NoDep of int
-  | Com
-
-type 'a substitution = (bindOcc * 'a) list
-
 type pf_status =
   | Complete_proof
   | Incomplete_proof
 
-type hyp_location = (* To distinguish body and type of local defs *)
-  | InHyp of identifier
-  | InHypType of identifier
-
 type prim_rule =
   | Intro of identifier
   | Intro_replacing of identifier
@@ -61,12 +56,11 @@ type 'a sigma = {
 type proof_tree = {
   status : pf_status;
   goal : goal;
-  ref : (rule * proof_tree list) option; 
-  subproof : proof_tree option }
+  ref : (rule * proof_tree list) option }
 
 and rule =
   | Prim of prim_rule
-  | Tactic of tactic_expression
+  | Tactic of tactic_expr * proof_tree
   | Change_evars
 
 and goal = evar_info
@@ -75,31 +69,35 @@ and tactic = goal sigma -> (goal list sigma * validation)
 
 and validation = (proof_tree list -> proof_tree)
 
+and tactic_expr =
+  (constr,
+   Closure.evaluable_global_reference,
+   inductive or_metanum,
+   identifier)
+     Tacexpr.gen_tactic_expr
+
+and atomic_tactic_expr =
+  (constr,
+   Closure.evaluable_global_reference,
+   inductive or_metanum,
+   identifier)
+     Tacexpr.gen_atomic_tactic_expr
+
 and tactic_arg =
-  | Command        of Coqast.t
-  | Constr         of constr
-  | OpenConstr     of Pretyping.open_constr
-  | Constr_context of constr
-  | Identifier     of identifier
-  | Qualid         of Nametab.qualid
-  | Integer        of int
-  | Clause         of hyp_location list
-  | Bindings       of Coqast.t substitution
-  | Cbindings      of constr   substitution 
-  | Quoted_string  of string
-  | Tacexp         of Coqast.t
-  | Tac            of tactic * Coqast.t
-  | Redexp         of Tacred.red_expr
-  | Fixexp         of identifier * int * Coqast.t
-  | Cofixexp       of identifier * Coqast.t
-  | Letpatterns    of (int list option * (identifier * int list) list)
-  | Intropattern   of intro_pattern
-
-and intro_pattern =
-  | WildPat
-  | IdPat   of identifier
-  | DisjPat of intro_pattern list
-  | ConjPat of intro_pattern list
-  | ListPat of intro_pattern list  
-
-and tactic_expression = string * tactic_arg list
+  (constr,
+   Closure.evaluable_global_reference,
+   inductive or_metanum,
+   identifier)
+     Tacexpr.gen_tactic_arg
+
+type hyp_location = identifier Tacexpr.raw_hyp_location
+
+type open_generic_argument =
+    (constr,raw_tactic_expr) generic_argument
+type closed_generic_argument =
+    (constr,raw_tactic_expr) generic_argument
+
+type 'a closed_abstract_argument_type =
+    ('a,constr,raw_tactic_expr) abstract_argument_type
+
+type declaration_hook = Nametab.strength -> Nametab.global_reference -> unit
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 60cd71092..b6a08ac8b 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -14,26 +14,18 @@ open Evd
 open Names
 open Term
 open Util
+open Tacexpr
+open Rawterm
+open Genarg
 (*i*)
 
 (* This module defines the structure of proof tree and the tactic type. So, it
    is used by [Proof_tree] and [Refiner] *)
 
-type bindOcc = 
-  | Dep of identifier
-  | NoDep of int
-  | Com
-
-type 'a substitution = (bindOcc * 'a) list
-
 type pf_status =
   | Complete_proof
   | Incomplete_proof
 
-type hyp_location = (* To distinguish body and type of local defs *)
-  | InHyp of identifier
-  | InHypType of identifier
-
 type prim_rule =
   | Intro of identifier
   | Intro_replacing of identifier
@@ -92,12 +84,11 @@ type 'a sigma = {
 type proof_tree = {
   status : pf_status;
   goal : goal;
-  ref : (rule * proof_tree list) option; 
-  subproof : proof_tree option }
+  ref : (rule * proof_tree list) option }
 
 and rule =
   | Prim of prim_rule
-  | Tactic of tactic_expression
+  | Tactic of tactic_expr * proof_tree
   | Change_evars
 
 and goal = evar_info
@@ -106,31 +97,35 @@ and tactic = goal sigma -> (goal list sigma * validation)
 
 and validation = (proof_tree list -> proof_tree)
 
+and tactic_expr =
+  (constr,
+   Closure.evaluable_global_reference,
+   inductive or_metanum,
+   identifier)
+     Tacexpr.gen_tactic_expr
+
+and atomic_tactic_expr =
+  (constr,
+   Closure.evaluable_global_reference,
+   inductive or_metanum,
+   identifier)
+     Tacexpr.gen_atomic_tactic_expr
+
 and tactic_arg =
-  | Command        of Coqast.t
-  | Constr         of constr
-  | OpenConstr     of Pretyping.open_constr
-  | Constr_context of constr
-  | Identifier     of identifier
-  | Qualid         of Nametab.qualid
-  | Integer        of int
-  | Clause         of hyp_location list
-  | Bindings       of Coqast.t substitution
-  | Cbindings      of constr   substitution 
-  | Quoted_string  of string
-  | Tacexp         of Coqast.t
-  | Tac            of tactic * Coqast.t
-  | Redexp         of Tacred.red_expr
-  | Fixexp         of identifier * int * Coqast.t
-  | Cofixexp       of identifier * Coqast.t
-  | Letpatterns    of (int list option * (identifier * int list) list)
-  | Intropattern   of intro_pattern
-
-and intro_pattern =
-  | WildPat
-  | IdPat   of identifier
-  | DisjPat of intro_pattern list
-  | ConjPat of intro_pattern list
-  | ListPat of intro_pattern list  
-
-and tactic_expression = string * tactic_arg list
+  (constr,
+   Closure.evaluable_global_reference,
+   inductive or_metanum,
+   identifier)
+     Tacexpr.gen_tactic_arg
+
+type hyp_location = identifier Tacexpr.raw_hyp_location
+
+type open_generic_argument =
+    (constr,raw_tactic_expr) generic_argument
+type closed_generic_argument =
+    (constr,raw_tactic_expr) generic_argument
+
+type 'a closed_abstract_argument_type =
+    ('a,constr,raw_tactic_expr) abstract_argument_type
+
+type declaration_hook = Nametab.strength -> Nametab.global_reference -> unit
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 7937b9913..b990e6f4b 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -22,6 +22,7 @@ open Type_errors
 open Proof_trees
 open Proof_type
 open Logic
+open Printer
 
 type transformation_tactic = proof_tree -> (goal list * validation)
 
@@ -98,7 +99,6 @@ let rec frontier p =
          (fun retpfl ->
             let pfl' = mapshape (List.map List.length gll) vl retpfl in
             { status = and_status (List.map pf_status pfl');
-              subproof = p.subproof;
               goal = p.goal;
               ref = Some(r,pfl')}))
 
@@ -120,7 +120,6 @@ let rec nb_unsolved_goals pf =
 
 let leaf g = {
   status = Incomplete_proof;
-  subproof = None;
   goal = g;
   ref = None }
 
@@ -130,8 +129,8 @@ let tac_tab = Hashtbl.create 17
 
 let add_tactic s t =
   if Hashtbl.mem tac_tab s then
-    errorlabstrm ("Refiner.add_tactic: "^s) 
-      (str "Cannot redeclare a tactic.");
+    errorlabstrm ("Refiner.add_tactic: ") 
+      (str ("Cannot redeclare tactic "^s));
   Hashtbl.add tac_tab s t
 
 let overwriting_add_tactic s t =
@@ -158,6 +157,16 @@ let check_subproof_connection gl spfl =
   if not (list_for_all2eq (fun g pf -> g=pf.goal) gl spfl)
   then (bad_subproof (); false) else true
 
+let abstract_tactic_expr te tacfun gls =
+  let (sgl_sigma,v) = tacfun gls in
+  let hidden_proof = v (List.map leaf sgl_sigma.it) in
+  (sgl_sigma,
+   fun spfl ->
+     assert (check_subproof_connection sgl_sigma.it spfl);
+     { status = and_status (List.map pf_status spfl);
+       goal = gls.it;
+       ref = Some(Tactic(te,hidden_proof),spfl) })
+
 let refiner = function
   | Prim pr as r ->
       let prim_fun = prim_refiner pr in
@@ -168,21 +177,9 @@ let refiner = function
 	     assert (check_subproof_connection sgl spfl);
              { status = and_status (List.map pf_status spfl);
                goal = goal_sigma.it;
-               subproof = None;
                ref = Some(r,spfl) })))
-      
-  | Tactic(s,targs) as r ->
-      let tacfun = lookup_tactic s targs in
-      (fun goal_sigma ->
-         let (sgl_sigma,v) = tacfun goal_sigma in
-         let hidden_proof = v (List.map leaf sgl_sigma.it) in
-         (sgl_sigma,
-          fun spfl ->
-	    assert (check_subproof_connection sgl_sigma.it spfl);
-            { status = and_status (List.map pf_status spfl);
-              goal = goal_sigma.it;
-              subproof = Some hidden_proof;
-              ref = Some(r,spfl) }))
+
+  | Tactic _ -> failwith "Refiner: should not occur"
       
    (* [Local_constraints lc] makes the local constraints be [lc] and
       normalizes evars *)
@@ -197,7 +194,6 @@ let refiner = function
 	          assert (check_subproof_connection [ngl] spfl);
                   { status = (List.hd spfl).status;
                     goal = gl;
-                    subproof = None;
                     ref = Some(r,spfl) }))
            (* if the evar change does not affect the goal, leave the
               proof tree unchanged *)
@@ -206,9 +202,22 @@ let refiner = function
                         assert (List.length spfl = 1);
                         List.hd spfl))))
 
-let vernac_tactic texp = refiner (Tactic texp)
 let norm_evar_tac gl = refiner Change_evars gl
 
+(*
+let vernac_tactic (s,args) =
+  let tacfun = lookup_tactic s args in
+  abstract_extra_tactic s args tacfun
+*)
+let abstract_tactic te = abstract_tactic_expr (Tacexpr.TacAtom (dummy_loc,te))
+
+let abstract_extended_tactic s args = 
+  abstract_tactic (Tacexpr.TacExtend (s, args))
+
+let vernac_tactic (s,args) =
+  let tacfun = lookup_tactic s args in
+  abstract_extended_tactic s args tacfun
+
 (* [rc_of_pfsigma : proof sigma -> readable_constraints] *)
 let rc_of_pfsigma sigma = rc_of_gc sigma.sigma sigma.it.goal
 
@@ -228,7 +237,7 @@ let extract_open_proof sigma pf =
   let rec proof_extractor vl = function
     | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf
 	  
-    | {ref=Some(Tactic _,spfl); subproof=Some hidden_proof} ->
+    | {ref=Some(Tactic (_,hidden_proof),spfl)} ->
 	let sgl,v = frontier hidden_proof in
 	let flat_proof = v spfl in
 	proof_extractor vl flat_proof
@@ -304,20 +313,37 @@ let start_tac gls =
 
 let finish_tac (sigr,gl,p) = (repackage sigr gl, p)
 
-let thens_tac tac2l taci (sigr,gs,p) =
-  let (gl,gi) =
-    try list_chop (List.length tac2l) gs
-    with Failure _ -> errorlabstrm "Refiner.combine_tactics"
-        (str "Wrong number of tactics.") in
-  let tac2gl =
-    List.combine gl tac2l @ list_map_i (fun i g -> (g, taci i)) 1 gi in
+(* Apply [taci.(i)] on the first n-th subgoals and [tac] on the others *)
+let thensf_tac taci tac (sigr,gs,p) =
+  let n = Array.length taci in
+  let nsg = List.length gs in
+  if nsg<n then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
+  let gll,pl =
+    List.split
+      (list_map_i (fun i -> apply_sig_tac sigr (if i<n then taci.(i) else tac))
+	0 gs) in
+  (sigr, List.flatten gll,
+   compose p (mapshape (List.map List.length gll) pl))
+
+(* Apply [taci.(i)] on the last n-th subgoals and [tac] on the others *)
+let thensl_tac tac taci (sigr,gs,p) =
+  let n = Array.length taci in
+  let nsg = List.length gs in
+  if nsg<n then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
   let gll,pl =
-    List.split(List.map (fun (g,tac2) -> apply_sig_tac sigr tac2 g) tac2gl) in
+    List.split
+      (list_map_i (fun i -> apply_sig_tac sigr (if i<0 then tac else taci.(i)))
+	(n-nsg) gs) in
   (sigr, List.flatten gll,
    compose p (mapshape (List.map List.length gll) pl))
 
-let then_tac tac = thens_tac [] (fun _ -> tac)
+(* Apply [tac i] on the ith subgoal (no subgoals number check) *)
+let thensi_tac tac (sigr,gs,p) =
+  let gll,pl =
+    List.split (list_map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs) in
+  (sigr, List.flatten gll, compose p (mapshape (List.map List.length gll) pl))
 
+let then_tac tac = thensf_tac [||] tac
 
 let non_existent_goal n =
   errorlabstrm ("No such goal: "^(string_of_int n))
@@ -330,42 +356,53 @@ let theni_tac i tac ((_,gl,_) as subgoals) =
   let k = if i < 0 then nsg + i + 1 else i in
   if nsg < 1 then errorlabstrm "theni_tac" (str"No more subgoals.")
   else if k >= 1 & k <= nsg then
-    thens_tac [] (fun i -> if i = k then tac else tclIDTAC) subgoals
+    thensf_tac
+      (Array.init k (fun i -> if i+1 = k then tac else tclIDTAC)) tclIDTAC
+      subgoals
   else non_existent_goal k 
 
-(* [tclTHENSi tac1 [t1 ; ... ; tn] taci gls] applies the tactic [tac1]
+(* [tclTHENSFIRSTn tac1 [|t1 ; ... ; tn|] tac2 gls] applies the tactic [tac1]
    to [gls] and applies [t1], ..., [tn] to the [n] first resulting
-   subgoals, and [(taci i)] to the (i+n)-th goal. Raises an error if
-   the number of resulting subgoals is less than [n] *)
-let tclTHENSi tac1 tac2l taci gls =
-  finish_tac (thens_tac tac2l taci (then_tac tac1 (start_tac gls)))
-
+   subgoals, and [tac2] to the others subgoals. Raises an error if
+   the number of resulting subgoals is strictly less than [n] *)
+let tclTHENSFIRSTn tac1 taci tac gls =
+  finish_tac (thensf_tac taci tac (then_tac tac1 (start_tac gls)))
+
+(* [tclTHENSLASTn tac1 tac2 [|t1 ;...; tn|] gls] applies the tactic [tac1]
+   to [gls] and applies [t1], ..., [tn] to the [n] last resulting
+   subgoals, and [tac2] to the other subgoals. Raises an error if the
+   number of resulting subgoals is strictly less than [n] *)
+let tclTHENSLASTn tac1 tac taci gls =
+  finish_tac (thensl_tac tac taci (then_tac tac1 (start_tac gls)))
+
+(* [tclTHEN_i tac taci gls] applies the tactic [tac] to [gls] and applies
+   [(taci i)] to the i_th resulting subgoal (starting from 1), whatever the
+   number of subgoals is *)
+let tclTHEN_i tac taci gls =
+  finish_tac (thensi_tac taci (then_tac tac (start_tac gls)))
+
+let tclTHENLASTn tac1 taci = tclTHENSLASTn tac1 tclIDTAC taci
+let tclTHENFIRSTn tac1 taci = tclTHENSFIRSTn tac1 taci tclIDTAC
 
 (* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
    [tac2] to every resulting subgoals *)
-let tclTHEN tac1 tac2 = tclTHENSi tac1 [] (fun _ -> tac2)
+let tclTHEN tac1 tac2 = tclTHENSFIRSTn tac1 [||] tac2
 
-(* [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
-   [(tac2 i)] to the i_th resulting subgoal (starting from 1) *)
-let tclTHEN_i tac1 tac2 = tclTHENSi tac1 [] tac2
-
-(* [tclTHENS tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to
+(* [tclTHENSV tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to
    [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
    an error if the number of resulting subgoals is not [n] *)
-let tclTHENS tac1 tac2l =
-  tclTHENSi tac1 tac2l (fun _ -> tclFAIL_s "Wrong number of tactics.")
-
-(* Same as [tclTHENS] but completes with [tac3] if the number resulting 
-   subgoals is strictly less than [n] *)
-let tclTHENST tac1 tac2l tac3 = tclTHENSi tac1 tac2l (fun _ -> tac3)
+let tclTHENSV tac1 tac2v =
+  tclTHENSFIRSTn tac1 tac2v (tclFAIL_s "Wrong number of tactics.")
 
-(* Same as tclTHENST but completes with [Idtac] *)
-let tclTHENSI tac1 tac2l = tclTHENST tac1 tac2l tclIDTAC
+let tclTHENS tac1 tac2l = tclTHENSV tac1 (Array.of_list tac2l)
 
-(* [tclTHENL tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
+(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
    to the last resulting subgoal *)
-let tclTHENL (tac1 : tactic) (tac2 : tactic) (gls : goal sigma) =
-  finish_tac (theni_tac (-1) tac2 (then_tac tac1 (start_tac gls)))
+let tclTHENLAST tac1 tac2 = tclTHENSLASTn tac1 tclIDTAC [|tac2|]
+
+(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
+   to the first resulting subgoal *)
+let tclTHENFIRST tac1 tac2 = tclTHENSFIRSTn tac1 [|tac2|] tclIDTAC
 
 
 (* [tclTHENLIST [t1;..;tn]] applies [t1] then [t2] ... then [tn]. More
@@ -473,7 +510,7 @@ let rec tclREPEAT t g =
 
 let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t))
 
-(* Repeat on the first subgoal *)
+(* Repeat on the first subgoal (no failure if no more subgoal) *)
 let rec tclREPEAT_MAIN t g =
   (tclORELSE (tclTHEN_i t (fun i -> if i = 1 then (tclREPEAT_MAIN t) else
     tclIDTAC)) tclIDTAC) g
@@ -590,7 +627,6 @@ let descend n p =
                        let newstatus = and_status (List.map pf_status spfl) in
                        { status   = newstatus;
 			 goal     = p.goal;
-			 subproof = p.subproof;
 			 ref      = Some(r,spfl) }
                      else 
 		       error "descend: validation"))
@@ -607,13 +643,13 @@ let traverse n pts = match n with
 	       tstack = tl;
 	       tpfsigma = pts.tpfsigma })
   | -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *)
-      (match pts.tpf.subproof with
-	 | None -> error "traverse: not a tactic-node"
-	 | Some spf ->
+      (match pts.tpf.ref with
+	 | Some (Tactic (_,spf),_) ->
 	     let v = (fun pfl -> pts.tpf) in 
 	     { tpf = spf;
                tstack = (-1,v)::pts.tstack;
-               tpfsigma = pts.tpfsigma })
+               tpfsigma = pts.tpfsigma }
+	 | _ -> error "traverse: not a tactic-node")
   | n -> (* when n>0, go to the nth child *)
       let (npf,v) = descend n pts.tpf in 
       { tpf = npf;
@@ -782,14 +818,15 @@ let rec top_of_tree pts =
 (* Pretty-printers. *)
 
 open Pp
-open Printer
 
-let pr_tactic (s,l) =
-  gentacpr (Ast.ope (s,(List.map ast_of_cvt_arg l)))
+let pr_tactic = function
+  | Tacexpr.TacArg (Tacexpr.Tacexp t) ->
+      Pptactic.pr_raw_tactic t (*top tactic from tacinterp*)
+  | t -> Pptactic.pr_tactic t
 
 let pr_rule = function
   | Prim r -> pr_prim_rule r
-  | Tactic texp -> hov 0 (pr_tactic texp)
+  | Tactic (texp,_) -> hov 0 (pr_tactic texp)
   | Change_evars ->
       (* This is internal tactic and cannot be replayed at user-level.
          Function pr_rule_dot below is used when we want to hide
@@ -798,8 +835,8 @@ let pr_rule = function
 
 (* Does not print change of evars *)
 let pr_rule_dot = function 
-  | Change_evars -> (mt ())
-  | r -> (pr_rule r ++ str"." ++ fnl ()) 
+  | Change_evars -> mt ()
+  | r -> pr_rule r ++ str"." ++ fnl ()
 
 exception Different
 
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 385d6e8b1..34f8fb665 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -1,3 +1,4 @@
+
 (***********************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
 (* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
@@ -14,6 +15,7 @@ open Sign
 open Evd
 open Proof_trees
 open Proof_type
+open Tacexpr
 (*i*)
 
 (* The refiner (handles primitive rules and high-level tactics). *)
@@ -30,12 +32,20 @@ val apply_sig_tac :
 
 type transformation_tactic = proof_tree -> (goal list * validation)
 
-val add_tactic             : string -> (tactic_arg list -> tactic) -> unit
-val overwriting_add_tactic : string -> (tactic_arg list -> tactic) -> unit
-val lookup_tactic          : string -> (tactic_arg list) -> tactic
+val add_tactic             : string -> (closed_generic_argument list -> tactic) -> unit
+val overwriting_add_tactic : string -> (closed_generic_argument list -> tactic) -> unit
+val lookup_tactic          : string -> (closed_generic_argument list) -> tactic
+
+(*s Hiding the implementation of tactics. *)
+
+(* [abstract_tactic tac] hides the (partial) proof produced by [tac] under
+   a single proof node *)
+val abstract_tactic : atomic_tactic_expr -> tactic -> tactic
+val abstract_tactic_expr : tactic_expr -> tactic -> tactic
+val abstract_extended_tactic : string -> closed_generic_argument list -> tactic -> tactic
 
 val refiner : rule -> tactic
-val vernac_tactic : tactic_expression -> tactic
+val vernac_tactic : string * closed_generic_argument list -> tactic
 val frontier : transformation_tactic
 val list_pf : proof_tree -> goal list
 val unTAC : tactic -> goal sigma -> proof_tree sigma
@@ -57,24 +67,44 @@ val tclTHENLIST      : tactic list -> tactic
    [(tac2 i)] to the [i]$^{th}$ resulting subgoal (starting from 1) *)
 val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
 
-(* [tclTHENL tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
-   to the last resulting subgoal *)
-val tclTHENL         : tactic -> tactic -> tactic
+(* [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
+   to the last resulting subgoal (previously called [tclTHENL]) *)
+val tclTHENLAST         : tactic -> tactic -> tactic
+
+(* [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
+   to the first resulting subgoal *)
+val tclTHENFIRST         : tactic -> tactic -> tactic
 
-(* [tclTHENS tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to
+(* [tclTHENS tac1 [|t1 ; ... ; tn|] gls] applies the tactic [tac1] to
    [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
    an error if the number of resulting subgoals is not [n] *)
+val tclTHENSV         : tactic -> tactic array -> tactic
+
+(* Same with a list of tactics *)
 val tclTHENS         : tactic -> tactic list -> tactic
 
-(* Same as [tclTHENS] but completes with [tac3] if the number resulting 
-   subgoals is strictly more than [n] *)
-val tclTHENST        : tactic -> tactic list -> tactic -> tactic
+(* [tclTHENST] is renamed [tclTHENSFIRSTn]
+val tclTHENST        : tactic -> tactic array -> tactic -> tactic
+*)
+
+(* [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the
+   last [n] resulting subgoals and [tac2] on the remaining first subgoals *)
+val tclTHENSLASTn     : tactic -> tactic -> tactic array -> tactic
 
-(* Same as [tclTHENS] but  completes with [tac3 i] *)
-val tclTHENSi        : tactic -> tactic list -> (int -> tactic) -> tactic
+(* [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then
+   applies [t1],...,[tn] on the first [n] resulting subgoals and
+   [tac2] for the remaining last subgoals (previously called tclTHENST) *)
+val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
 
-(* Same as tclTHENST but completes with [Idtac] *)
-val tclTHENSI        : tactic -> tactic list -> tactic
+(* [tclTHENLASTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then,
+   applies [t1],...,[tn] on the last [n] resulting subgoals and leaves
+   unchanged the other subgoals *)
+val tclTHENLASTn    : tactic -> tactic array -> tactic
+
+(* [tclTHENFIRSTn tac1 [t1 ; ... ; tn] gls] first applies [tac1] then,
+   applies [t1],...,[tn] on the first [n] resulting subgoals and leaves
+   unchanged the other subgoals (previously called [tclTHENSI]) *)
+val tclTHENFIRSTn   : tactic -> tactic array -> tactic
 
 (* A special exception for levels for the Fail tactic *)
 exception FailError of int
@@ -95,7 +125,6 @@ val tclWEAK_PROGRESS : tactic -> tactic
 val tclNOTSAMEGOAL   : tactic -> tactic
 val tclINFO          : tactic -> tactic
 
-
 (*s Tactics handling a list of goals. *)
 
 type validation_list = proof_tree list -> proof_tree list
@@ -152,8 +181,8 @@ open Pp
 (*i*)
 
 val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds
-val pr_rule      : rule -> std_ppcmds
-val pr_tactic    : tactic_expression -> std_ppcmds
+val pr_rule     : rule -> std_ppcmds
+val pr_tactic   : tactic_expr -> std_ppcmds
 val print_script :
   bool -> evar_map -> named_context -> proof_tree -> std_ppcmds
 val print_treescript :
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 238dd4b95..b6fea7dc2 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -19,6 +19,7 @@ open Inductive
 open Reduction
 open Environ
 open Declare
+open Refiner
 open Tacmach
 open Clenv
 open Pattern
@@ -29,24 +30,39 @@ open Wcclausenv
 (*         Basic Tacticals                *)
 (******************************************)
 
-let tclIDTAC         = Tacmach.tclIDTAC
-let tclORELSE        = Tacmach.tclORELSE
-let tclTHEN          = Tacmach.tclTHEN
-let tclTHEN_i        = Tacmach.tclTHEN_i
-let tclTHENL         = Tacmach.tclTHENL
-let tclTHENS         = Tacmach.tclTHENS
-let tclTHENSi        = Tacmach.tclTHENSi
-let tclREPEAT        = Tacmach.tclREPEAT
-let tclFIRST         = Tacmach.tclFIRST
-let tclSOLVE         = Tacmach.tclSOLVE
-let tclTRY           = Tacmach.tclTRY
-let tclINFO          = Tacmach.tclINFO
-let tclCOMPLETE      = Tacmach.tclCOMPLETE
-let tclAT_LEAST_ONCE = Tacmach.tclAT_LEAST_ONCE
-let tclFAIL          = Tacmach.tclFAIL
-let tclDO            = Tacmach.tclDO
-let tclPROGRESS      = Tacmach.tclPROGRESS
-let tclWEAK_PROGRESS = Tacmach.tclWEAK_PROGRESS
+(*************************************************)
+(* Tacticals re-exported from the Refiner module.*)
+(*************************************************)
+
+let tclIDTAC         = tclIDTAC
+let tclORELSE        = tclORELSE
+let tclTHEN          = tclTHEN
+let tclTHENLIST      = tclTHENLIST
+let tclTHEN_i        = tclTHEN_i
+let tclTHENFIRST     = tclTHENFIRST
+let tclTHENLAST      = tclTHENLAST
+let tclTHENS         = tclTHENS
+let tclTHENSV        = Refiner.tclTHENSV
+let tclTHENSFIRSTn   = Refiner.tclTHENSFIRSTn
+let tclTHENSLASTn    = Refiner.tclTHENSLASTn
+let tclTHENFIRSTn    = Refiner.tclTHENFIRSTn
+let tclTHENLASTn     = Refiner.tclTHENLASTn
+let tclREPEAT        = Refiner.tclREPEAT
+let tclREPEAT_MAIN   = tclREPEAT_MAIN
+let tclFIRST         = Refiner.tclFIRST
+let tclSOLVE         = Refiner.tclSOLVE
+let tclTRY           = Refiner.tclTRY
+let tclINFO          = Refiner.tclINFO
+let tclCOMPLETE      = Refiner.tclCOMPLETE
+let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
+let tclFAIL          = Refiner.tclFAIL
+let tclDO            = Refiner.tclDO
+let tclPROGRESS      = Refiner.tclPROGRESS
+let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
+let tclNOTSAMEGOAL   = Refiner.tclNOTSAMEGOAL
+let tclTHENTRY       = tclTHENTRY
+
+let unTAC            = unTAC
 
 (* [rclTHENSEQ [t1;..;tn] is equivalent to t1;..;tn *)
 let tclTHENSEQ = List.fold_left tclTHEN tclIDTAC
@@ -56,10 +72,6 @@ let tclTHENSEQ = List.fold_left tclTHEN tclIDTAC
 let tclMAP tacfun l = 
   List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
 
-(*let dyn_tclIDTAC = function [] -> tclIDTAC |  _ -> anomaly "tclIDTAC"*)
-
-(*let dyn_tclFAIL  = function [] -> tclFAIL |  _ -> anomaly "tclFAIL"*)
-
 (* apply a tactic to the nth element of the signature  *)
 
 let tclNTH_HYP m (tac : constr->tactic) gl =
@@ -187,30 +199,6 @@ let tryAllHyps     tac gls = tryClauses tac (allHyps gls) gls
 let onNLastHyps n  tac     = onHyps (nLastHyps n) (tclMAP tac)
 let onLastHyp      tac gls = tac (lastHyp gls) gls
 
-(* Serait-ce possible de compiler d'abord la tactique puis de faire la
-   substitution sans passer par bdize dont l'objectif est de préparer un
-   terme pour l'affichage ? (HH) *)
-
-(* Si on enlève le dernier argument (gl) conclPattern est calculé une
-fois pour toutes : en particulier si Pattern.somatch produit une UserError 
-Ce qui fait que si la conclusion ne matche pas le pattern, Auto échoue, même
-si après Intros la conclusion matche le pattern.
-*)
-
-(* conclPattern doit échouer avec error car il est rattraper par tclFIRST *)
-
-let conclPattern concl pat tacast gl =
-  let constr_bindings =
-    try Pattern.matches pat concl
-    with PatternMatchingFailure -> error "conclPattern" in
-  let ast_bindings = 
-    List.map 
-      (fun (i,c) ->
-	 (i, Termast.ast_of_constr false (pf_env gl) c))
-      constr_bindings in 
-  let tacast' = Coqast.subst_meta ast_bindings tacast in
-  Tacinterp.interp tacast' gl
-
 let clauseTacThen tac continuation =
   (fun cls -> (tclTHEN (tac cls) continuation))
 
@@ -252,7 +240,7 @@ type branch_args = {
 
 type branch_assumptions = {
   ba        : branch_args;     (* the branch args *)
-  assums    : named_context; (* the list of assumptions introduced *)
+  assums    : named_context;   (* the list of assumptions introduced *)
   cargs     : identifier list; (* the constructor arguments *)
   constargs : identifier list; (* the CONSTANT constructor arguments *)
   recargs   : identifier list; (* the RECURSIVE constructor arguments *)
@@ -337,24 +325,25 @@ let general_elim_then_using
   let branchsigns = elim_sign_fun ity in
   let after_tac ce i gl =
     let (hd,largs) = decompose_app (clenv_template_type ce).rebus in
-    let ba = { branchsign = branchsigns.(i-1);
+    let ba = { branchsign = branchsigns.(i);
                nassums = 
 		 List.fold_left 
                    (fun acc b -> if b then acc+2 else acc+1)
-                   0 branchsigns.(i-1);
-               branchnum = i;
+                   0 branchsigns.(i);
+               branchnum = i+1;
                ity = ity;
                largs = List.map (clenv_instance_term ce) largs;
                pred = clenv_instance_term ce hd }
     in 
     tac ba gl
   in
+  let branchtacs ce = Array.init (Array.length branchsigns) (after_tac ce) in
   let elimclause' =
     match predicate with
        | None   -> elimclause'
        | Some p -> clenv_assign pmv p elimclause'
   in 
-  elim_res_pf_THEN_i kONT elimclause' after_tac gl
+  elim_res_pf_THEN_i kONT elimclause' branchtacs gl
 
 
 let elimination_then_using tac predicate (indbindings,elimbindings) c gl = 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 90cb04f3e..0557be882 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -25,12 +25,19 @@ open Wcclausenv
 val tclIDTAC         : tactic
 val tclORELSE        : tactic -> tactic -> tactic
 val tclTHEN          : tactic -> tactic -> tactic
+val tclTHENSEQ       : tactic list -> tactic
+val tclTHENLIST      : tactic list -> tactic
 val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
-val tclTHENL         : tactic -> tactic -> tactic
+val tclTHENFIRST     : tactic -> tactic -> tactic
+val tclTHENLAST      : tactic -> tactic -> tactic
 val tclTHENS         : tactic -> tactic list -> tactic
-val tclTHENSi        : tactic -> tactic list -> (int -> tactic) -> tactic
-val tclTHENSEQ       : tactic list -> tactic
+val tclTHENSV        : tactic -> tactic array -> tactic
+val tclTHENSLASTn    : tactic -> tactic -> tactic array -> tactic
+val tclTHENLASTn     : tactic -> tactic array -> tactic
+val tclTHENSFIRSTn   : tactic -> tactic array -> tactic -> tactic
+val tclTHENFIRSTn    : tactic -> tactic array -> tactic
 val tclREPEAT        : tactic -> tactic
+val tclREPEAT_MAIN   : tactic -> tactic
 val tclFIRST         : tactic list -> tactic
 val tclSOLVE         : tactic list -> tactic
 val tclTRY           : tactic -> tactic
@@ -41,16 +48,16 @@ val tclFAIL          : int -> tactic
 val tclDO            : int -> tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
+val tclNOTSAMEGOAL   : tactic -> tactic
+val tclTHENTRY       : tactic -> tactic -> tactic
+
 val tclNTH_HYP       : int -> (constr -> tactic) -> tactic
 val tclMAP           : ('a -> tactic) -> 'a list -> tactic
 val tclLAST_HYP      : (constr -> tactic) -> tactic
 val tclTRY_sign      : (constr -> tactic) -> named_context -> tactic
 val tclTRY_HYPS      : (constr -> tactic) -> tactic
 
-(*i
-val dyn_tclIDTAC     : tactic_arg list -> tactic
-val dyn_tclFAIL      : tactic_arg list -> tactic
-i*)
+val unTAC            : tactic -> goal sigma -> proof_tree sigma
 
 (*s Clause tacticals. *)
 
@@ -59,10 +66,6 @@ type clause = identifier option
 val nth_clause  : int -> goal sigma -> clause
 val clause_type : clause -> goal sigma -> constr
 
-(*i
-val matches      : goal sigma -> constr -> marked_term -> bool
-val dest_match   : goal sigma -> constr -> marked_term -> constr list
-i*)
 val pf_matches : goal sigma -> constr_pattern -> constr -> (int * constr) list
 val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 
@@ -95,13 +98,6 @@ val tryAllHyps     : (identifier -> tactic) -> tactic
 val onNLastHyps    : int -> (named_declaration -> tactic) -> tactic
 val onLastHyp      : (identifier -> tactic) -> tactic
 
-(* [ConclPattern concl pat tacast]:
-   if the term concl matches the pattern pat, (in sense of 
-   [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the
-   right values to build a tactic *)
-
-val conclPattern : constr -> constr_pattern -> Coqast.t -> tactic
-
 (*s Elimination tacticals. *)
 
 type branch_args = {