modifs pour premiere edition de liens

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

12 files changed, 164 insertions, 452 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 80aae11823..5f6af5a8b3 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -56,10 +56,10 @@ let applyHead n c wc =
         | DOP2(Prod,c1,c2) ->
             let c1ty = w_type_of wc c1 in
 	    let evar = new_evar_in_sign (w_env wc) in
-            let (evar_sp, _) = destConst evar in
+            let (evar_n, _) = destEvar evar in
 	    (compose 
 	       (apprec (n-1) (applist(c,[evar])) (sAPP c2 evar))
-	       (w_Declare evar_sp (DOP2(Cast,c1,c1ty))))
+	       (w_Declare evar_n (DOP2(Cast,c1,c1ty))))
 	    wc
 	| _ -> error "Apply_Head_Then"
   in 
@@ -243,20 +243,20 @@ and w_resrec metas evars wc =
 	  
     | (lhs,(DOP0(Meta k) as rhs))::t -> w_resrec ((k,lhs)::metas) t wc
 	  
-    | (DOPN(Const evsp,_) as evar,rhs)::t ->
+    | (DOPN(Evar evn,_) as evar,rhs)::t ->
 	if w_defined_const wc evar then
           let (wc',metas') = w_Unify rhs evar metas wc in 
 	  w_resrec metas' t wc'
 	else
           (try 
-	     w_resrec metas t (w_Define evsp rhs wc)
+	     w_resrec metas t (w_Define evn rhs wc)
            with UserError _ ->
              (match rhs with
              	| DOPN(AppL,cl) ->
 		    (match cl.(0) with
 		       | DOPN(Const sp,_) ->
 			   let wc' = mimick_evar cl.(0) 
-				       ((Array.length cl) - 1) evsp wc in
+				       ((Array.length cl) - 1) evn wc in
 			   w_resrec metas evars wc'
 		       | _ -> error "w_Unify")
 		| _ -> error "w_Unify"))
@@ -555,13 +555,13 @@ and clenv_resrec metas evars clenv =
     | ((lhs,(DOP0(Meta k) as rhs))::t,metas) ->
     	clenv_resrec ((k,lhs)::metas) t clenv
 	  
-    | ((DOPN(Const evsp,_) as evar,rhs)::t,metas) ->
+    | ((DOPN(Evar evn,_) as evar,rhs)::t,metas) ->
     	if w_defined_const clenv.hook evar then
           let (metas',evars') = unify_0 [] clenv.hook rhs evar in
           clenv_resrec (metas'@metas) (evars'@t) clenv
     	else
           (try 
-	     clenv_resrec metas t (clenv_wtactic (w_Define evsp rhs) clenv)
+	     clenv_resrec metas t (clenv_wtactic (w_Define evn rhs) clenv)
            with UserError _ ->
              (match rhs with
 		| DOPN(AppL,cl) ->
@@ -569,7 +569,7 @@ and clenv_resrec metas evars clenv =
 		       | (DOPN(Const _,_) | DOPN(MutConstruct _,_)) ->
 			   clenv_resrec metas evars 
 			     (clenv_wtactic (mimick_evar cl.(0) 
-					       ((Array.length cl) - 1) evsp) 
+					       ((Array.length cl) - 1) evn) 
 				clenv)
 		       | _ -> error "w_Unify")
            	| _ -> error "w_Unify"))
@@ -857,10 +857,10 @@ let clenv_pose_dependent_evars clenv =
   List.fold_left
     (fun clenv mv ->
        let evar = new_evar_in_sign (w_env clenv.hook) in
-       let (evar_sp,_) = destConst evar in
+       let (evar_n,_) = destEvar evar in
        let tY = clenv_instance_type clenv mv in
        let tYty = w_type_of clenv.hook tY in
-       let clenv' = clenv_wtactic (w_Declare evar_sp (DOP2(Cast,tY,tYty))) 
+       let clenv' = clenv_wtactic (w_Declare evar_n (DOP2(Cast,tY,tYty))) 
 		      clenv in
        clenv_assign mv evar clenv')
     clenv
@@ -909,13 +909,13 @@ and clenv_resrec metas evars clenv =
     | ((lhs,(DOP0(Meta k) as rhs))::t,metas) ->
     	clenv_resrec ((k,lhs)::metas) t clenv
 
-    | ((DOPN(Const evsp,_) as evar,rhs)::t,metas) ->
+    | ((DOPN(Evar evn,_) as evar,rhs)::t,metas) ->
     	if w_defined_const clenv.hook evar then
           let (metas',evars') = unify_0 [] clenv.hook rhs evar in
           clenv_resrec (metas'@metas) (evars'@t) clenv
     	else
           (try 
-	     clenv_resrec metas t (clenv_wtactic (w_Define evsp rhs) clenv)
+	     clenv_resrec metas t (clenv_wtactic (w_Define evn rhs) clenv)
            with UserError _ ->
              (match rhs with
 		| DOPN(AppL,cl) ->
@@ -923,7 +923,7 @@ and clenv_resrec metas evars clenv =
 		       | (DOPN(Const _,_) |  DOPN(MutConstruct _,_)) ->
 			   clenv_resrec metas evars 
 			     (clenv_wtactic (mimick_evar cl.(0) 
-					       ((Array.length cl) - 1) evsp) 
+					       ((Array.length cl) - 1) evn) 
 				clenv)
 		       | _ -> error "w_Unify")
            	| _ -> error "w_Unify"))
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index e63648576d..e43d519665 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -61,7 +61,7 @@ let restore_decl sp evd evc =
   let newgoal = { evar_env = evd.evar_env; 
 		  evar_concl = evd.evar_concl;
 		  evar_body = evd.evar_body;
-                  evar_info = newctxt } in
+                  evar_info = Some newctxt } in
   (rc_add evc (sp,newgoal))
 
 
@@ -114,6 +114,7 @@ let w_Focus sp wc = ids_mod (extract_decl sp) wc
 let w_Underlying wc = (ts_it (ids_it wc)).decls
 let w_type_of wc c  = ctxt_type_of (ids_it wc) c
 let w_env     wc    = get_env (ids_it wc)
+let w_hyps    wc    = var_context (get_env (ids_it wc))
 let w_ORELSE wt1 wt2 wc = try wt1 wc with UserError _ -> wt2 wc
 
 let w_Declare sp c (wc:walking_constraints) =
@@ -153,7 +154,7 @@ let w_Define sp c wc =
     	let access = evars_of (ids_it wc) c in
     	let spdecl' = { evar_env = spdecl.evar_env;
                        	evar_concl = spdecl.evar_concl;
-                       	evar_info = mt_ctxt access;
+                       	evar_info = Some (mt_ctxt access);
                        	evar_body = Evar_defined c }
     	in 
 	(ids_mod (fun evc -> (Proof_trees.remap evc (sp,spdecl'))) wc)
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 47bba83fa3..620c9c4b8c 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -38,6 +38,7 @@ val w_Define     : evar -> constr -> w_tactic
 
 val w_Underlying : walking_constraints -> evar_declarations
 val w_env        : walking_constraints -> env
+val w_hyps       : walking_constraints -> var_context
 val w_type_of    : walking_constraints -> constr -> constr
 val w_add_sign   : (identifier * typed_type) -> walking_constraints 
                      -> walking_constraints
diff --git a/proofs/logic.ml b/proofs/logic.ml
index db3a6ca18d..8a04322828 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -40,7 +40,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     | DOP0(Meta mv) ->
 	if occur_meta conclty then
           error "Cannot refine to conclusions with meta-variables";
-	let ctxt = goal.evar_info in 
+	let ctxt = out_some goal.evar_info in 
 	(mk_goal ctxt env (nf_betaiota env sigma conclty))::goalacc, conclty
 
     | DOP2(Cast,t,ty) ->
@@ -80,7 +80,7 @@ and mk_hdgoals sigma goal goalacc trm =
   match trm with
     | DOP2(Cast,DOP0(Meta mv),ty) ->
 	let _ = type_of env sigma ty in
-	let ctxt = goal.evar_info in  
+	let ctxt = out_some goal.evar_info in  
 	(mk_goal ctxt env (nf_betaiota env sigma ty))::goalacc,ty
 	  
     | DOPN(AppL,cl) ->
@@ -217,7 +217,7 @@ let prim_refiner r sigma goal =
   let env = goal.evar_env in
   let sign = var_context env in
   let cl = goal.evar_concl in
-  let info = goal.evar_info in
+  let info = out_some goal.evar_info in
   match r with
     | { name = Intro; newids = [id] } ->
     	if mem_sign sign id then error "New variable is already declared";
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 663aedb44d..8bdecdf8fc 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -96,23 +96,24 @@ let lc_toList lc = Intset.elements lc
 (* Functions on goals *)
 
 let mk_goal ctxt env cl = 
-  { evar_env = env; evar_concl = cl; evar_body = Evar_empty; evar_info = ctxt }
+  { evar_env = env; evar_concl = cl; 
+    evar_body = Evar_empty; evar_info = Some ctxt }
 
 (* Functions on the information associated with existential variables  *)
 
 let mt_ctxt lc = { pgm = None; mimick = None; lc = lc }
 
-let get_ctxt gl = gl.evar_info
+let get_ctxt gl = out_some gl.evar_info
 
-let get_pgm gl = gl.evar_info.pgm
+let get_pgm gl = (out_some gl.evar_info).pgm
 
 let set_pgm pgm ctxt = { ctxt with pgm = pgm }
 
-let get_mimick gl = gl.evar_info.mimick
+let get_mimick gl = (out_some gl.evar_info).mimick
 
 let set_mimick mimick ctxt = { mimick = mimick; pgm = ctxt.pgm; lc = ctxt.lc }
 
-let get_lc gl = gl.evar_info.lc
+let get_lc gl = (out_some gl.evar_info).lc
 
 (* Functions on proof trees *)
 
@@ -225,6 +226,12 @@ let ctxt_access sigma sp =
   lc_exists (fun sp' -> sp' = sp or mentions sigma sp sp') (ts_it sigma).focus
 
 
+let pf_lookup_name_as_renamed hyps ccl s =
+  Termast.lookup_name_as_renamed (gLOB hyps) ccl s
+
+let pf_lookup_index_as_renamed ccl n =
+  Termast.lookup_index_as_renamed ccl n
+
 (*********************************************************************)
 (*                  Pretty printing functions                        *)
 (*********************************************************************)
@@ -299,7 +306,13 @@ let pr_pgm ctxt = match ctxt.pgm with
 let pr_ctxt ctxt =
   let pc = pr_pgm ctxt in [< 'sTR"[" ; pc; 'sTR"]" >]
 
-let pr_seq {evar_env=env; evar_concl=cl; evar_info=info} =
+let pr_seq evd = 
+  let env = evd.evar_env
+  and cl = evd.evar_concl
+  and info = match evd.evar_info with 
+    | Some i -> i 
+    | None -> anomaly "pr_seq : info = None"
+  in
   let (x,y) as hyps = var_context env in
   let sign = List.rev(List.combine x y) in
   let pc = pr_ctxt info in
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 6e0f179b0e..5e268c320f 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -144,6 +144,10 @@ val get_gc    : readable_constraints -> global_constraints
 val remap     : readable_constraints -> int * goal -> readable_constraints
 val ctxt_access : readable_constraints -> int -> bool
 
+val pf_lookup_name_as_renamed : 
+  var_context -> constr -> identifier -> int option
+val pf_lookup_index_as_renamed : constr -> int -> int option
+
 
 (*s Pretty printing functions. *)
 
@@ -156,15 +160,15 @@ val pr_subgoals  : goal list -> std_ppcmds
 val pr_subgoal   : int -> goal list -> std_ppcmds
 
 val pr_decl      : goal -> std_ppcmds
-val pr_decls     : global_constraints ->std_ppcmds
+val pr_decls     : global_constraints -> std_ppcmds
 val pr_evc       : readable_constraints -> std_ppcmds
 
 val prgl         : goal -> std_ppcmds
 val pr_seq       : goal -> std_ppcmds
 val pr_focus     : local_constraints -> std_ppcmds
 val pr_ctxt      : ctxtty -> std_ppcmds
-val pr_evars     : (int * goal) list ->  std_ppcmds
-val pr_evars_int : int -> (int * goal) list ->  std_ppcmds
+val pr_evars     : (int * goal) list -> std_ppcmds
+val pr_evars_int : int -> (int * goal) list -> std_ppcmds
 val pr_subgoals_existential : evar_declarations -> goal list -> std_ppcmds
 
 val ast_of_cvt_arg : tactic_arg ->  Coqast.t 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index dac2d6a61c..aeccbc0947 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -177,7 +177,7 @@ let refiner = function
   | (Local_constraints lc) as r ->
       (fun goal_sigma ->
          let gl = goal_sigma.it  in
-         let ctxt = gl.evar_info in 
+         let ctxt = out_some gl.evar_info in 
          let sg = mk_goal ctxt gl.evar_env gl.evar_concl in
 	 ({it=[sg];sigma=goal_sigma.sigma},
           (fun pfl -> 
@@ -346,6 +346,12 @@ let tclTHEN (tac1:tactic) (tac2:tactic) (gls:goal sigma) =
   (repackage sigr (List.flatten gll), 
    compose p (mapshape(List.map List.length gll)pl))
 
+(* tclTHENLIST [t1;..;tn] applies t1;..tn. More convenient than tclTHEN
+   when n is large. *)
+let rec tclTHENLIST = function
+  | [] -> tclIDTAC
+  | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl)
+
 (* tclTHEN_i tac1 tac2 n gls applies the tactic tac1 to gls and applies
    tac2 (i+n-1) to the i_th resulting subgoal *)
 
@@ -928,3 +934,15 @@ let print_subscript sigma sign pf =
   else 
     format_print_info_script sigma sign pf
 
+let tclINFO (tac:tactic) gls = 
+  let (sgl,v) as res = tac gls in 
+  begin try 
+    let pf = v (List.map leaf (sig_it sgl)) in
+    let sign = var_context (sig_it gls).evar_env in
+    mSGNL(hOV 0 [< 'sTR" == "; 
+                   print_subscript 
+                     ((compose ts_it sig_sig) gls) sign pf >])
+  with UserError _ -> 
+    mSGNL(hOV 0 [< 'sTR "Info failed to apply validation" >])
+  end;
+  res
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index fa80f4329e..4d1edc7e5b 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -55,6 +55,7 @@ val extract_open_proof :
 val tclIDTAC         : tactic
 val tclORELSE        : tactic -> tactic -> tactic
 val tclTHEN          : tactic -> tactic -> tactic
+val tclTHENLIST      : tactic list -> tactic
 val tclTHEN_i        : tactic -> (int -> tactic) -> int -> tactic
 val tclTHENL         : tactic -> tactic -> tactic
 val tclTHENS         : tactic -> tactic list -> tactic
@@ -71,6 +72,7 @@ val tclDO            : int -> tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
 val tclNOTSAMEGOAL   : tactic -> tactic
+val tclINFO          : tactic -> tactic
 
 
 (*s Tactics handling a list of goals. *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b70320b81a..49315aba7c 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -40,6 +40,7 @@ let sig_it     = Refiner.sig_it
 let sig_sig    = Refiner.sig_sig
 let project    = compose ts_it sig_sig
 let pf_env gls = (sig_it gls).evar_env
+let pf_hyps gls = var_context (sig_it gls).evar_env
 
 let pf_concl gls = (sig_it gls).evar_concl
 
@@ -71,11 +72,18 @@ let pf_check_type gls c1 c2 =
 
 let pf_constr_of_com gls c =
   let evc = project gls in 
-  Astterm.constr_of_com evc (sig_it gls).hyps c
+  Astterm.constr_of_com evc (sig_it gls).evar_env c
 
 let pf_constr_of_com_sort gls c =
   let evc = project gls in 
-  Astterm.constr_of_com_sort evc (sig_it gls).hyps c
+  Astterm.constr_of_com_sort evc (sig_it gls).evar_env c
+
+let pf_global gls id = Declare.global (sig_it gls).evar_env id
+let pf_parse_const gls = compose (pf_global gls) id_of_string
+
+let pf_execute gls =
+  let evc = project gls in 
+  Typing.unsafe_machine (sig_it gls).evar_env evc
 
 let pf_reduction_of_redexp gls re c = 
   reduction_of_redexp re (pf_env gls) (project gls) c 
@@ -91,8 +99,8 @@ let pf_nf_betaiota               = pf_reduce nf_betaiota
 let pf_compute                   = pf_reduce compute
 let pf_unfoldn ubinds            = pf_reduce (unfoldn ubinds)
 
-let pf_conv_x                   = pf_reduce conv
-let pf_conv_x_leq               = pf_reduce conv_leq
+let pf_conv_x                   = pf_reduce is_conv
+let pf_conv_x_leq               = pf_reduce is_conv_leq
 let pf_const_value              = pf_reduce (fun env _ -> constant_value env)
 let pf_one_step_reduce          = pf_reduce one_step_reduce
 let pf_reduce_to_mind           = pf_reduce reduce_to_mind
@@ -163,6 +171,7 @@ let w_Declare_At    = w_Declare_At
 let w_Define        = w_Define
 let w_Underlying    = w_Underlying
 let w_env           = w_env
+let w_hyps          = w_hyps
 let w_type_of       = w_type_of
 let w_IDTAC         = w_IDTAC
 let w_ORELSE        = w_ORELSE
@@ -171,7 +180,7 @@ let ctxt_type_of    = ctxt_type_of
 
 let w_defined_const wc k     = defined_constant (w_env wc) k
 let w_const_value wc         = constant_value (w_env wc)
-let w_conv_x wc m n          = conv (w_env wc) (w_Underlying wc) m n
+let w_conv_x wc m n          = is_conv (w_env wc) (w_Underlying wc) m n
 let w_whd_betadeltaiota wc c = whd_betadeltaiota (w_env wc) (w_Underlying wc) c
 let w_hnf_constr wc c        = hnf_constr (w_env wc) (w_Underlying wc) c
 
@@ -182,23 +191,25 @@ let w_hnf_constr wc c        = hnf_constr (w_env wc) (w_Underlying wc) c
 
 let tclIDTAC         = tclIDTAC
 let tclORELSE        = tclORELSE
-let tclTHEN          =  tclTHEN
-let tclTHEN_i        =  tclTHEN_i
-let tclTHENL         =  tclTHENL
-let tclTHENS         =  tclTHENS
-let tclTHENSI        =  tclTHENSI
-let tclREPEAT        =  tclREPEAT
-let tclFIRST         =  tclFIRST
-let tclSOLVE         =  tclSOLVE
-let tclTRY           =  tclTRY
-let tclTHENTRY       =  tclTHENTRY
-let tclCOMPLETE      =  tclCOMPLETE
-let tclAT_LEAST_ONCE =  tclAT_LEAST_ONCE
-let tclFAIL          =  tclFAIL
-let tclDO            =  tclDO
-let tclPROGRESS      =  tclPROGRESS
+let tclTHEN          = tclTHEN
+let tclTHENLIST      = tclTHENLIST
+let tclTHEN_i        = tclTHEN_i
+let tclTHENL         = tclTHENL
+let tclTHENS         = tclTHENS
+let tclTHENSI        = tclTHENSI
+let tclREPEAT        = tclREPEAT
+let tclFIRST         = tclFIRST
+let tclSOLVE         = tclSOLVE
+let tclTRY           = tclTRY
+let tclTHENTRY       = tclTHENTRY
+let tclCOMPLETE      = tclCOMPLETE
+let tclAT_LEAST_ONCE = tclAT_LEAST_ONCE
+let tclFAIL          = tclFAIL
+let tclDO            = tclDO
+let tclPROGRESS      = tclPROGRESS
 let tclWEAK_PROGRESS = tclWEAK_PROGRESS
 let tclNOTSAMEGOAL   = tclNOTSAMEGOAL
+let tclINFO          = tclINFO
 
 let unTAC            = unTAC
 
@@ -266,6 +277,35 @@ let add_tactic = Refiner.add_tactic
 let overwriting_tactic = Refiner.overwriting_add_tactic
 
 
+(* Some combinators for parsing tactic arguments. 
+   They transform the Coqast.t arguments of the tactic into 
+   constr arguments *)
+
+type ('a,'b) parse_combinator = ('a -> tactic) -> ('b -> tactic)
+
+let tactic_com tac t x = tac (pf_constr_of_com x t) x
+      
+let tactic_com_sort tac t x = tac (pf_constr_of_com_sort x t) x
+      
+let tactic_com_list tac tl x =
+  let translate = pf_constr_of_com x in 
+  tac (List.map translate tl) x
+    
+let tactic_bind_list tac tl x =
+  let translate = pf_constr_of_com x in 
+  tac (List.map (fun (b,c)->(b,translate c)) tl) x
+
+let tactic_com_bind_list tac (c,tl) x =
+  let translate = pf_constr_of_com x in 
+  tac (translate c,List.map (fun (b,c')->(b,translate c')) tl) x
+
+let tactic_com_bind_list_list tac args gl =
+  let translate (c,tl) = 
+    (pf_constr_of_com gl c,
+     List.map (fun (b,c')->(b,pf_constr_of_com gl c')) tl) in 
+  tac (List.map translate args) gl
+
+
 (********************************************************)
 (* Functions for hiding the implementation of a tactic. *)
 (********************************************************)
@@ -279,7 +319,6 @@ let overwrite_hidden_tactic s tac  =
   overwriting_add_tactic s tac;
   (fun args -> vernac_tactic(s,args))
 
-(*** 
 let tactic_com = 
   fun tac t x -> tac (pf_constr_of_com x t) x
       
@@ -427,7 +466,6 @@ let hide_cbindll_tactic s tac =
   in 
   add_tactic s tacfun;
   fun l -> vernac_tactic(s,putconstrbinds l)
-***)
 
 
 (* Pretty-printers *)
@@ -437,8 +475,8 @@ open Printer
 
 let pr_com sigma goal com =
   prterm (rename_bound_var 
-            (ids_of_sign goal.hyps) 
-            (Trad.constr_of_com sigma goal.hyps com))
+            (ids_of_sign (var_context goal.evar_env)) 
+            (Astterm.constr_of_com sigma goal.evar_env com))
 
 let pr_one_binding sigma goal = function
   | (Dep id,com)  -> [< print_id id ; 'sTR":=" ; pr_com sigma goal com >]
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index fd4388876a..4593e92b77 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -30,7 +30,7 @@ val apply_sig_tac :
 
 val pf_concl              : goal sigma -> constr
 val pf_env                : goal sigma -> env
-val pf_hyps               : goal sigma -> typed_type signature
+val pf_hyps               : goal sigma -> var_context
 val pf_untyped_hyps       : goal sigma -> constr signature
 val pf_nth_hyp            : goal sigma -> int -> identifier * constr
 val pf_ctxt               : goal sigma -> ctxtty
@@ -38,7 +38,7 @@ val pf_global             : goal sigma -> identifier -> constr
 val pf_parse_const        : goal sigma -> string -> constr
 val pf_type_of            : goal sigma -> constr -> constr
 val pf_check_type         : goal sigma -> constr -> constr -> constr
-val pf_fexecute           : goal sigma -> constr -> unsafe_judgment
+val pf_execute            : goal sigma -> constr -> unsafe_judgment
 val hnf_type_of           : goal sigma -> constr -> constr
 
 val pf_constr_of_com      : goal sigma -> Coqast.t -> constr
@@ -48,10 +48,15 @@ val pf_get_hyp             : goal sigma -> identifier -> constr
 
 val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
 
-val pf_reduce : 'a reduction_function -> goal sigma -> constr -> constr
+
+
+val pf_reduce : 
+  (env -> evar_declarations -> constr -> constr) ->
+    goal sigma -> constr -> constr
 
 val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
-val pf_whd_betadeltaiota_stack : goal sigma -> 'a stack_reduction_function
+val pf_whd_betadeltaiota_stack : 
+  goal sigma -> constr -> constr list -> constr * constr list 
 val pf_hnf_constr              : goal sigma -> constr -> constr
 val pf_red_product             : goal sigma -> constr -> constr
 val pf_nf                      : goal sigma -> constr -> constr
@@ -107,6 +112,7 @@ val change_constraints_pftreestate :
 val tclIDTAC         : tactic
 val tclORELSE        : tactic -> tactic -> tactic
 val tclTHEN          : tactic -> tactic -> tactic
+val tclTHENLIST      : tactic list -> tactic
 val tclTHEN_i        : tactic -> (int -> tactic) -> int -> tactic
 val tclTHENL         : tactic -> tactic -> tactic
 val tclTHENS         : tactic -> tactic list -> tactic
@@ -172,14 +178,14 @@ val startWalk :
 
 val walking_THEN        : 'a result_w_tactic -> ('a -> tactic) -> tactic
 val walking             : w_tactic -> tactic
-val w_Focusing_THEN     : section_path -> 'a result_w_tactic 
+val w_Focusing_THEN     : int -> 'a result_w_tactic 
                           -> ('a -> w_tactic) -> w_tactic
-val w_Declare           : section_path -> constr -> w_tactic
-val w_Declare_At        : section_path -> section_path -> constr -> w_tactic
-val w_Define            : section_path -> constr -> w_tactic
+val w_Declare           : int -> constr -> w_tactic
+val w_Declare_At        : int -> int -> constr -> w_tactic
+val w_Define            : int -> constr -> w_tactic
 val w_Underlying        : walking_constraints -> evar_declarations
 val w_env               : walking_constraints -> env
-val w_hyps              : walking_constraints -> context
+val w_hyps              : walking_constraints -> var_context
 val w_type_of           : walking_constraints -> constr -> constr
 val w_add_sign          : (identifier * typed_type) 
                           -> walking_constraints -> walking_constraints
@@ -199,6 +205,26 @@ val add_tactic         : string -> (tactic_arg list -> tactic) -> unit
 val overwriting_tactic : string -> (tactic_arg list -> tactic) -> unit
 
 
+(*s Transformation of tactic arguments. *)
+
+type ('a,'b) parse_combinator = ('a -> tactic) -> ('b -> tactic)
+
+val tactic_com       : (constr,Coqast.t) parse_combinator
+val tactic_com_sort  : (constr,Coqast.t) parse_combinator
+val tactic_com_list  : (constr list, Coqast.t list) parse_combinator
+
+val tactic_bind_list : ((bindOcc * constr) list,
+                        (bindOcc * Coqast.t) list) parse_combinator
+
+val tactic_com_bind_list : 
+  (constr   * (bindOcc * constr)   list,
+   Coqast.t * (bindOcc * Coqast.t) list) parse_combinator
+
+val tactic_com_bind_list_list :  
+  ((constr   * (bindOcc * constr)   list) list, 
+   (Coqast.t * (bindOcc * Coqast.t) list) list) parse_combinator
+
+
 (*s Hiding the implementation of tactics. *)
 
 val hide_tactic  : 
diff --git a/proofs/tacred.ml b/proofs/tacred.ml
deleted file mode 100644
index 16ea6c5896..0000000000
--- a/proofs/tacred.ml
+++ /dev/null
@@ -1,353 +0,0 @@
-
-(* $Id$ *)
-
-open Pp
-open Util
-open Names
-open Generic
-open Term
-open Inductive
-open Environ
-open Reduction
-open Instantiate
-open Redinfo
-
-exception Elimconst
-exception Redelimination
-
-let is_elim c =
-  let (sp, _) = destConst c in
-  match constant_eval sp with
-    | NotAnElimination -> raise Elimconst
-    | Elimination (lv,n,b) -> (lv,n,b)
-
-let rev_firstn_liftn fn ln = 
-  let rec rfprec p res l = 
-    if p = 0 then 
-      res 
-    else
-      match l with
-        | [] -> invalid_arg "Reduction.rev_firstn_liftn"
-        | a::rest -> rfprec (p-1) ((lift ln a)::res) rest
-  in 
-  rfprec fn []
-
-let make_elim_fun f largs =
-  try 
-    let (lv,n,b) = is_elim f 
-    and ll = List.length largs in 
-    if ll < n then raise Redelimination;
-    if b then
-      let labs,_ = list_chop n largs in
-      let p = List.length lv in
-      let la' = list_map_i 
-		  (fun q aq ->
-		     try (Rel (p+1-(list_index (n+1-q) (List.map fst lv)))) 
-		     with Failure _ -> aq) 1
-                  (List.map (lift p) labs) 
-      in
-      list_fold_left_i 
-	(fun i c (k,a) -> 
-           DOP2(Lambda,(substl (rev_firstn_liftn (n-k) (-i) la') a),
-                DLAM(Name(id_of_string"x"),c))) 0 (applistc f la') lv
-    else 
-      f
-  with Elimconst | Failure _ -> 
-    raise Redelimination
-
-let mind_nparams env i =
-  let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams
-
-(* F is convertible to DOPN(Fix(recindices,bodynum),bodyvect) make 
-   the reduction using this extra information *)
-
-let contract_fix_use_function f fix =
-  match fix with 
-    | DOPN(Fix(recindices,bodynum),bodyvect) ->
-  	let nbodies = Array.length recindices in
-  	let make_Fi j = DOPN(Fix(recindices,j),bodyvect) in
-  	let lbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
-	  sAPPViList bodynum (array_last bodyvect) lbodies
-    | _ -> assert false
-
-let reduce_fix_use_function f whfun fix stack =
-  match fix with 
-    | DOPN (Fix(recindices,bodynum),bodyvect) ->
-	(match fix_recarg fix stack with
-           | None -> (false,(fix,stack))
-	   | Some (recargnum,recarg) ->
-               let (recarg'hd,_ as recarg')= whfun recarg [] in
-               let stack' = list_assign stack recargnum (applist recarg') in
-	       (match recarg'hd with
-                  | DOPN(MutConstruct _,_) ->
-		      (true,(contract_fix_use_function f fix,stack'))
-		  | _ -> (false,(fix,stack'))))
-    | _ -> assert false
-
-let contract_cofix_use_function f cofix =
-  match cofix with 
-    | DOPN(CoFix(bodynum),bodyvect) ->
-  	let nbodies =  (Array.length bodyvect) -1 in
-  	let make_Fi j = DOPN(CoFix(j),bodyvect) in
-  	let lbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
-  	sAPPViList bodynum (array_last bodyvect) lbodies
-    | _ -> assert false
-
-let reduce_mind_case_use_function env f mia =
-  match mia.mconstr with 
-    | DOPN(MutConstruct((indsp,tyindx),i),_) ->
-	let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in
-	let nparams = mind_nparams env ind in
-	let real_cargs = snd(list_chop nparams mia.mcargs) in
-	applist (mia.mlf.(i-1),real_cargs)
-    | DOPN(CoFix _,_) as cofix ->
-	let cofix_def = contract_cofix_use_function f cofix in
-	mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf
-    | _ -> assert false
-	  
-let special_red_case env whfun p c ci lf  =
-  let rec redrec c l = 
-    let (constr,cargs) = whfun c l in 
-    match constr with 
-      | DOPN(Const _,_) as g -> 
-          if evaluable_constant env g then
-            let gvalue = constant_value env g in
-            if reducible_mind_case gvalue then
-              reduce_mind_case_use_function env g
-                {mP=p; mconstr=gvalue; mcargs=cargs; mci=ci; mlf=lf}
-            else 
-	      redrec gvalue cargs
-          else 
-	    raise Redelimination
-      | _ ->
-          if reducible_mind_case constr then
-            reduce_mind_case env
-              {mP=p; mconstr=constr; mcargs=cargs; mci=ci; mlf=lf}
-          else 
-	    raise Redelimination
-  in 
-  redrec c []
-
-let rec red_elim_const env sigma k largs =
-  if not (evaluable_constant env k) then raise Redelimination;
-  let f = make_elim_fun k largs in
-  match whd_betadeltaeta_stack env sigma (constant_value env k) largs with
-    | (DOPN(MutCase _,_) as mc,lrest) ->
-        let (ci,p,c,lf) = destCase mc in
-        (special_red_case env (construct_const env sigma) p c ci lf, lrest)
-    | (DOPN(Fix _,_) as fix,lrest) -> 
-        let (b,(c,rest)) = 
-	  reduce_fix_use_function f (construct_const env sigma) fix lrest
-        in 
-	if b then (nf_beta env sigma c, rest) else raise Redelimination
-    | _ -> assert false
-
-and construct_const env sigma c stack = 
-  let rec hnfstack x stack =
-    match x with
-      | (DOPN(Const _,_)) as k  ->
-          (try
-             let (c',lrest) = red_elim_const env sigma k stack in 
-	     hnfstack c' lrest
-           with Redelimination ->
-             if evaluable_constant env k then 
-	       let cval = constant_value env k in
-	       (match cval with
-                  | DOPN (CoFix _,_) -> (k,stack)
-                  | _ -> hnfstack cval stack) 
-             else 
-	       raise Redelimination)
-      | (DOPN(Abst _,_) as a) ->
-          if evaluable_abst env a then 
-	    hnfstack (abst_value env a) stack
-          else 
-	    raise Redelimination
-      | DOP2(Cast,c,_) -> hnfstack c stack
-      | DOPN(AppL,cl) -> hnfstack (array_hd cl) (array_app_tl cl stack)
-      | DOP2(Lambda,_,DLAM(_,c)) ->
-          (match stack with 
-             | [] -> assert false
-             | c'::rest -> stacklam hnfstack [c'] c rest)
-      | DOPN(MutCase _,_) as c_0 ->
-          let (ci,p,c,lf) = destCase c_0 in
-          hnfstack 
-	    (special_red_case env (construct_const env sigma) p c ci lf) 
-	    stack
-      | DOPN(MutConstruct _,_) as c_0 -> c_0,stack
-      | DOPN(CoFix _,_) as c_0 -> c_0,stack
-      | DOPN(Fix (_) ,_) as fix -> 
-          let (reduced,(fix,stack')) = reduce_fix hnfstack fix stack in 
-	  if reduced then hnfstack fix stack' else raise Redelimination
-      | _ -> raise Redelimination
-  in 
-  hnfstack c stack
-
-(* Hnf reduction tactic: *)
-
-let hnf_constr env sigma c = 
-  let rec redrec x largs =
-    match x with
-      | DOP2(Lambda,t,DLAM(n,c)) ->
-          (match largs with
-             | []      -> applist(x,largs)
-             | a::rest -> stacklam redrec [a] c rest)
-      | DOPN(AppL,cl)   -> redrec (array_hd cl) (array_app_tl cl largs)
-      | DOPN(Const _,_) ->
-          (try
-             let (c',lrest) = red_elim_const env sigma x largs in 
-	     redrec c' lrest
-           with Redelimination ->
-             if evaluable_constant env x then
-               let c = constant_value env x in
-	       (match c with 
-                  | DOPN(CoFix _,_) -> applist(x,largs)
-		  | _ ->  redrec c largs)
-             else 
-	       applist(x,largs))
-      | DOPN(Abst _,_) ->
-          if evaluable_abst env x then 
-	    redrec (abst_value env x) largs
-          else 
-	    applist(x,largs)
-      | DOP2(Cast,c,_) -> redrec c largs
-      | DOPN(MutCase _,_) ->
-          let (ci,p,c,lf) = destCase x in
-          (try
-             redrec 
-	       (special_red_case env (whd_betadeltaiota_stack env sigma) 
-		  p c ci lf) largs
-           with Redelimination -> 
-	     applist(x,largs))
-      | (DOPN(Fix _,_)) ->
-          let (reduced,(fix,stack)) = 
-            reduce_fix (whd_betadeltaiota_stack env sigma) x largs
-          in 
-	  if reduced then redrec fix stack else applist(x,largs)
-      | _ -> applist(x,largs)
-  in 
-  redrec c []
-
-(* Simpl reduction tactic: same as simplify, but also reduces
-   elimination constants *)
-
-let whd_nf env sigma c = 
-  let rec nf_app c stack =
-    match c with
-      | DOP2(Lambda,c1,DLAM(name,c2))    ->
-          (match stack with
-             | [] -> (c,[])
-             | a1::rest -> stacklam nf_app [a1] c2 rest)
-      | DOPN(AppL,cl) -> nf_app (array_hd cl) (array_app_tl cl stack)
-      | DOP2(Cast,c,_) -> nf_app c stack
-      | DOPN(Const _,_) ->
-          (try
-             let (c',lrest) = red_elim_const env sigma c stack in 
-	     nf_app c' lrest
-           with Redelimination -> 
-	     (c,stack))
-      | DOPN(MutCase _,_) ->
-          let (ci,p,d,lf) = destCase c in
-          (try
-             nf_app (special_red_case env nf_app p d ci lf) stack
-           with Redelimination -> 
-	     (c,stack))
-      | DOPN(Fix _,_) ->
-          let (reduced,(fix,rest)) = reduce_fix nf_app c stack in 
-	  if reduced then nf_app fix rest else (fix,stack)
-      | _ -> (c,stack)
-  in 
-  applist (nf_app c [])
-
-let nf env sigma c = strong whd_nf env sigma c
-
-(* Generic reduction: reduction functions used in reduction tactics *)
-
-type red_expr =
-  | Red
-  | Hnf
-  | Simpl
-  | Cbv of Closure.flags
-  | Lazy of Closure.flags
-  | Unfold of (int list * section_path) list
-  | Fold of constr list
-  | Change of constr
-  | Pattern of (int list * constr * constr) list
-
-let reduction_of_redexp = function
-  | Red -> red_product
-  | Hnf -> hnf_constr
-  | Simpl -> nf
-  | Cbv f -> cbv_norm_flags f
-  | Lazy f -> clos_norm_flags f
-  | Unfold ubinds -> unfoldn ubinds
-  | Fold cl -> fold_commands cl
-  | Change t -> (fun _ _ _ -> t)
-  | Pattern lp -> pattern_occs lp
-
-(* Used in several tactics. *)
-
-let one_step_reduce env sigma = 
-  let rec redrec largs x =
-    match x with
-      | DOP2(Lambda,t,DLAM(n,c))  ->
-          (match largs with
-             | []      -> error "Not reducible 1"
-             | a::rest -> applistc (subst1 a c) rest)
-      | DOPN(AppL,cl) -> redrec (array_app_tl cl largs) (array_hd cl)
-      | DOPN(Const _,_) ->
-          (try
-             let (c',l) = red_elim_const env sigma x largs in applistc c' l
-           with Redelimination ->
-             if evaluable_constant env x then
-               applistc (constant_value env x) largs
-             else error "Not reductible 1")
-      | DOPN(Abst _,_) ->
-          if evaluable_abst env x then applistc (abst_value env x) largs
-          else error "Not reducible 0"
-      | DOPN(MutCase _,_) ->
-          let (ci,p,c,lf) = destCase x in
-          (try
-	     applistc 
-	       (special_red_case env (whd_betadeltaiota_stack env sigma) 
-		  p c ci lf) largs 
-           with Redelimination -> error "Not reducible 2")
-      | DOPN(Fix _,_) ->
-          let (reduced,(fix,stack)) = 
-	    reduce_fix (whd_betadeltaiota_stack env sigma) x largs
-          in 
-	  if reduced then applistc fix stack else error "Not reducible 3"
-      | DOP2(Cast,c,_) -> redrec largs c
-      | _ -> error "Not reducible 3"
-  in 
-  redrec []
-
-(* put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name
-   return name, B and t' *)
-
-let reduce_to_mind env sigma t = 
-  let rec elimrec t l = 
-    match whd_castapp_stack t [] with
-      | (DOPN(MutInd _,_) as mind,_) -> (mind,t,prod_it t l)
-      | (DOPN(Const _,_),_) -> 
-          (try 
-	     let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in 
-	     elimrec t' l
-           with UserError _ -> errorlabstrm "tactics__reduce_to_mind"
-               [< 'sTR"Not an inductive product : it is a constant." >])
-      | (DOPN(MutCase _,_),_) ->
-          (try 
-	     let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in 
-	     elimrec t' l
-           with UserError _ -> errorlabstrm "tactics__reduce_to_mind"
-               [< 'sTR"Not an inductive product:"; 'sPC;
-		  'sTR"it is a case analysis term" >])
-      | (DOP2(Cast,c,_),[]) -> elimrec c l
-      | (DOP2(Prod,ty,DLAM(n,t')),[]) -> elimrec t' ((n,ty)::l)
-      | _ -> error "Not an inductive product"
- in 
- elimrec t []
-
-let reduce_to_ind env sigma t =
-  let (mind,redt,c) = reduce_to_mind env sigma t in 
-  (Declare.mind_path mind, redt, c)
-
diff --git a/proofs/tacred.mli b/proofs/tacred.mli
deleted file mode 100644
index a1aec82cdd..0000000000
--- a/proofs/tacred.mli
+++ /dev/null
@@ -1,38 +0,0 @@
-
-(* $Id$ *)
-
-(*i*)
-open Names
-open Term
-open Environ
-open Evd
-open Reduction
-(*i*)
-
-(* Reduction functions associated to tactics. \label{tacred} *)
-
-val hnf_constr : 'a reduction_function
-
-val nf : 'a reduction_function
-
-val one_step_reduce : 'a reduction_function
-
-val reduce_to_mind : 
-  env -> 'a evar_map -> constr -> constr * constr * constr
-
-val reduce_to_ind : 
-  env -> 'a evar_map -> constr -> section_path * constr * constr
-
-type red_expr =
-  | Red
-  | Hnf
-  | Simpl
-  | Cbv of Closure.flags
-  | Lazy of Closure.flags
-  | Unfold of (int list * section_path) list
-  | Fold of constr list
-  | Change of constr
-  | Pattern of (int list * constr * constr) list
-
-val reduction_of_redexp : red_expr -> 'a reduction_function
-