Cleaning/uniformizing the interface of tacticals.mli

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

18 files changed, 182 insertions, 227 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 75b811d518..adfb9ce2ff 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -1015,7 +1015,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
       (tclDO nb_intro_to_do intro)
       (
 	fun g' -> 
-	  let just_introduced = nLastHyps nb_intro_to_do g' in 
+	  let just_introduced = nLastDecls nb_intro_to_do g' in 
 	  let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in 
 	  tclTHEN (Equality.rewriteLR equation_lemma) (revert just_introduced_id) g'
       )
@@ -1218,7 +1218,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	    [
 	      (* observe_tac ("introducing args") *) (tclDO nb_args intro);
 	      (fun g -> (* replacement of the function by its body *)
-		 let args = nLastHyps nb_args g in 
+		 let args = nLastDecls nb_args g in 
 		 let fix_body = fix_info.body_with_param in
 (* 		 observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *)
 		 let args_id = List.map (fun (id,_,_) -> id) args in
@@ -1282,7 +1282,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	    [
 	      tclDO nb_args intro;
 	      (fun g -> (* replacement of the function by its body *)
-		 let args = nLastHyps nb_args g in 
+		 let args = nLastDecls nb_args g in 
 		 let args_id = List.map (fun (id,_,_) -> id) args in
 		 let dyn_infos = 
 		   {
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index 100868a0e5..aee133f6d9 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -769,9 +769,9 @@ let termination_proof_header is_mes input_type ids args_id relation
 	     (* rest of the proof *)
 	     tclTHENSEQ 
 	       [observe_tac "generalize" 
-		  (onNLastHyps (nargs+1)
-		     (fun (id,_,_) -> 
-			tclTHEN (h_generalize [mkVar id]) (h_clear false [id])
+		  (onNLastHypsId (nargs+1)
+		     (tclMAP (fun id -> 
+			tclTHEN (h_generalize [mkVar id]) (h_clear false [id]))
 		     ))
 	       ;
 		observe_tac "h_fix" (h_fix (Some hrec) (nargs+1));
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 483453cb30..17020c46d0 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -519,15 +519,15 @@ let blast_simpl = (free_try (reduce (Simpl None) onConcl))
 ;;
 let blast_induction1 = 
     (free_try (tclTHEN (tclTRY intro)
-		       (tclTRY (tclLAST_HYP simplest_elim))))
+		       (tclTRY (onLastHyp simplest_elim))))
 ;;
 let blast_induction2 = 
     (free_try (tclTHEN (tclTRY (tclTHEN intro intro))
-		       (tclTRY (tclLAST_HYP simplest_elim))))
+		       (tclTRY (onLastHyp simplest_elim))))
 ;;
 let blast_induction3 = 
     (free_try (tclTHEN (tclTRY (tclTHEN intro (tclTHEN intro intro)))
-		       (tclTRY (tclLAST_HYP simplest_elim))))
+		       (tclTRY (onLastHyp simplest_elim))))
 ;;
 
 blast_tactic :=
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index d35fb199be..b236f04d75 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -1,4 +1,20 @@
 =========================================
+= CHANGES BETWEEN COQ V8.2 AND COQ V8.3 =
+=========================================
+
+** Cleaning in tactical.mli
+
+tclLAST_HYP -> onLastHyp
+tclLAST_DECL -> onLastDecl
+tclLAST_NHYPS -> onNLastHypsId
+tclNTH_DECL -> onNthDecl
+tclNTH_HYP -> onNthHyp
+onLastHyp -> onLastHypId
+onNLastHyps -> onNLastDecls
+
++ removal of various unused combinators on type "clause"
+
+=========================================
 = CHANGES BETWEEN COQ V8.1 AND COQ V8.2 =
 =========================================
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 7a66067cd7..9dd35a8c23 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -448,8 +448,9 @@ let rec tclTHENLIST = function
     [] -> tclIDTAC
   | t1::tacl -> tclTHEN t1 (tclTHENLIST tacl)
 
-
-
+(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
+let tclMAP tacfun l = 
+  List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
 
 (* various progress criterions *)
 let same_goal gl subgoal = 
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 1823514270..5cbc2bde8f 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -80,6 +80,9 @@ val tclTHEN          : tactic -> tactic -> tactic
    convenient than [tclTHEN] when [n] is large *)
 val tclTHENLIST      : tactic list -> tactic
 
+(* [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
+val tclMAP           : ('a -> tactic) -> 'a list -> tactic
+
 (* [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
    [(tac2 i)] to the [i]$^{th}$ resulting subgoal (starting from 1) *)
 val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index f9b7b8677d..fa22de7bb2 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -111,11 +111,14 @@ let pf_const_value              = pf_reduce (fun env _ -> constant_value env)
 let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
 let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
-let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls)
+let pf_hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls)
 
 let pf_check_type gls c1 c2 = 
   ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2)))
 
+let pf_is_matching              = pf_apply Matching.is_matching_conv
+let pf_matches                  = pf_apply Matching.matches_conv
+
 (************************************)
 (* Tactics handling a list of goals *)
 (************************************)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index f57b121dba..826337cc8d 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -21,6 +21,7 @@ open Refiner
 open Redexpr
 open Tacexpr
 open Rawterm
+open Pattern
 (*i*)
 
 (* Operations for handling terms under a local typing context. *)
@@ -51,7 +52,7 @@ val pf_global             : goal sigma -> identifier -> constr
 val pf_parse_const        : goal sigma -> string -> constr
 val pf_type_of            : goal sigma -> constr -> types
 val pf_check_type         : goal sigma -> constr -> types -> unit
-val hnf_type_of           : goal sigma -> constr -> types
+val pf_hnf_type_of        : goal sigma -> constr -> types
 
 val pf_interp_constr      : goal sigma -> Topconstr.constr_expr -> constr
 val pf_interp_type        : goal sigma -> Topconstr.constr_expr -> types
@@ -86,6 +87,9 @@ val pf_const_value : goal sigma -> constant -> constr
 val pf_conv_x      : goal sigma -> constr -> constr -> bool
 val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
 
+val pf_matches     : goal sigma -> constr_pattern -> constr -> patvar_map
+val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
+
 type transformation_tactic = proof_tree -> (goal list * validation)
 
 val frontier : transformation_tactic
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 36e8add7e9..1398a335af 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -951,7 +951,7 @@ and intros_decomp p kont decls db n =
   if n = 0 then
     decomp_and_register_decls p kont decls db
   else
-    tclTHEN intro (tclLAST_DECL (fun d ->
+    tclTHEN intro (onLastDecl (fun d ->
       (intros_decomp p kont (d::decls) db (n-1))))
 
 (* Decompose hypotheses [hyps] with maximum depth [p] and
diff --git a/tactics/elim.ml b/tactics/elim.ml
index ae6e486e24..fd5d65d853 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -75,9 +75,9 @@ let elimHypThen tac id gl =
   elimination_then tac ([],[]) (mkVar id) gl
 
 let rec general_decompose_on_hyp recognizer =
-  ifOnHyp recognizer (general_decompose recognizer) (fun _ -> tclIDTAC)
+  ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> tclIDTAC)
 
-and general_decompose recognizer id =
+and general_decompose_aux recognizer id =
   elimHypThen
     (introElimAssumsThen
        (fun bas ->
@@ -97,8 +97,8 @@ let general_decompose recognizer c gl =
   let typc = pf_type_of gl c in  
   tclTHENSV (cut typc) 
     [| tclTHEN (intro_using tmphyp_name)
-         (onLastHyp
-	    (ifOnHyp recognizer (general_decompose recognizer)
+         (onLastHypId
+	    (ifOnHyp recognizer (general_decompose_aux recognizer)
 	      (fun id -> clear [id])));
        exact_no_check c |] gl
 
@@ -155,12 +155,12 @@ let simple_elimination c gls =
 let induction_trailer abs_i abs_j bargs =
   tclTHEN 
     (tclDO (abs_j - abs_i) intro)
-    (onLastHyp
+    (onLastHypId
        (fun id gls ->
 	  let idty = pf_type_of gls (mkVar id) in
 	  let fvty = global_vars (pf_env gls) idty in
 	  let possible_bring_hyps =
-	    (List.tl (nLastHyps (abs_j - abs_i) gls)) @ bargs.assums
+	    (List.tl (nLastDecls (abs_j - abs_i) gls)) @ bargs.assums
           in
 	  let (hyps,_) =
             List.fold_left 
@@ -184,7 +184,7 @@ let double_ind h1 h2 gls =
     if abs_i > abs_j then (abs_j,abs_i) else
       error "Both hypotheses are the same." in
   (tclTHEN (tclDO abs_i intro)
-     (onLastHyp
+     (onLastHypId
        	(fun id ->
            elimination_then
              (introElimAssumsThen (induction_trailer abs_i abs_j))
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 625a096625..9f5da99a7f 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -56,7 +56,7 @@ open Coqlib
    Eduardo Gimenez (30/3/98).
 *)
 
-let clear_last = (tclLAST_HYP (fun c -> (clear [destVar c])))
+let clear_last = (onLastHyp (fun c -> (clear [destVar c])))
 
 let choose_eq eqonleft = 
   if eqonleft then h_simplest_left else h_simplest_right
@@ -68,14 +68,14 @@ let mkBranches c1 c2 =
     [generalize [c2];
      h_simplest_elim c1;
      intros;
-     tclLAST_HYP h_simplest_case;
+     onLastHyp h_simplest_case;
      clear_last;
      intros]
 
 let solveNoteqBranch side = 
   tclTHEN (choose_noteq side)
     (tclTHEN (intro_force true)
-      (onLastHyp (fun id -> Extratactics.h_discrHyp id)))
+      (onLastHypId (fun id -> Extratactics.h_discrHyp id)))
 
 let h_solveNoteqBranch side =
   Refiner.abstract_extended_tactic "solveNoteqBranch" [] 
@@ -103,7 +103,7 @@ let mkGenDecideEqGoal rectype g =
 
 let eqCase tac = 
   (tclTHEN intro  
-  (tclTHEN (tclLAST_HYP Equality.rewriteLR)
+  (tclTHEN (onLastHyp Equality.rewriteLR)
   (tclTHEN clear_last 
   tac)))
 
@@ -176,7 +176,7 @@ let compare c1 c2 g =
   let decide  = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 g in  
   (tclTHENS (cut decide) 
             [(tclTHEN  intro 
-             (tclTHEN (tclLAST_HYP simplest_case)
+             (tclTHEN (onLastHyp simplest_case)
                        clear_last));
              decideEquality c1 c2]) g
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0d81879843..0ebe44197f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -269,7 +269,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl =
     let sym = build_coq_eq_sym () in
     let eq = applist (e, [t1;c1;c2]) in
     tclTHENS (assert_as false None eq)
-      [onLastHyp (fun id -> 
+      [onLastHypId (fun id -> 
 	tclTHEN 
 	  (tclTRY (general_multi_rewrite false false (inj_open (mkVar id),NoBindings) clause))
 	  (clear [id]));
@@ -541,7 +541,7 @@ let rec build_discriminator sigma env dirn c sort = function
 *)
 
 let gen_absurdity id gl =
-  if is_empty_type (clause_type (onHyp id) gl)
+  if is_empty_type (pf_get_hyp_typ gl id)
   then
     simplest_elim (mkVar id) gl
   else
@@ -585,7 +585,7 @@ let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort =
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
   let pf = clenv_value_cast_meta absurd_clause in
   tclTHENS (cut_intro absurd_term)
-    [onLastHyp gen_absurdity; refine pf]
+    [onLastHypId gen_absurdity; refine pf]
 
 let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls =
   let sigma =  eq_clause.evd in
@@ -616,7 +616,7 @@ let onNegatedEquality with_evars tac gls =
   match kind_of_term (hnf_constr (pf_env gls) (project gls) ccl) with
   | Prod (_,t,u) when is_empty_type u ->
       tclTHEN introf
-        (onLastHyp (fun id -> 
+        (onLastHypId (fun id -> 
           onEquality with_evars tac (mkVar id,NoBindings))) gls
   | _ -> 
       errorlabstrm "" (str "Not a negated primitive equality.")
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ca98cbc6f4..a0d1d27830 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -324,7 +324,7 @@ let projectAndApply thin id eqname names depids gls =
 	   (intro_move idopt no_move)
 	   (* try again to substitute and if still not a variable after *)
 	   (* decomposition, arbitrarily try to rewrite RL !? *)
-	   (tclTRY (onLastHyp (substHypIfVariable (subst_hyp false)))))
+	   (tclTRY (onLastHypId (substHypIfVariable (subst_hyp false)))))
 	 names);
        (if names = [] then clear [id] else tclIDTAC)]
   in
@@ -342,12 +342,12 @@ let rewrite_equations_gene othin neqns ba gl =
   let rewrite_eqns =
     match othin with
       | Some thin ->
-          onLastHyp
+          onLastHypId
             (fun last ->
               tclTHENSEQ
                 [tclDO neqns
                      (tclTHEN intro
-                        (onLastHyp
+                        (onLastHypId
                            (fun id ->
                               tclTRY 
 			        (projectAndApply thin id (ref no_move)
@@ -361,8 +361,8 @@ let rewrite_equations_gene othin neqns ba gl =
     [tclDO neqns intro;
      bring_hyps nodepids;
      clear (ids_of_named_context nodepids);
-     onHyps (compose List.rev (nLastHyps neqns)) bring_hyps;
-     onHyps (nLastHyps neqns) (compose clear ids_of_named_context);
+     onHyps (compose List.rev (nLastDecls neqns)) bring_hyps;
+     onHyps (nLastDecls neqns) (compose clear ids_of_named_context);
      rewrite_eqns;
      tclMAP (fun (id,_,_ as d) ->
                (tclORELSE (clear [id])
@@ -408,13 +408,13 @@ let rewrite_equations othin neqns names ba gl =
     match othin with
       | Some thin ->
           tclTHENSEQ
-            [onHyps (compose List.rev (nLastHyps neqns)) bring_hyps;
-             onHyps (nLastHyps neqns) (compose clear ids_of_named_context);
+            [onHyps (compose List.rev (nLastDecls neqns)) bring_hyps;
+             onHyps (nLastDecls neqns) (compose clear ids_of_named_context);
 	     tclMAP_i neqns (fun o ->
 	       let idopt,names = extract_eqn_names o in
                (tclTHEN
 		 (intro_move idopt no_move)
-		 (onLastHyp (fun id ->
+		 (onLastHypId (fun id ->
 		   tclTRY (projectAndApply thin id first_eq names depids)))))
 	       names;
 	     tclMAP (fun (id,_,_) gl ->
@@ -473,7 +473,7 @@ let raw_inversion inv_kind id status names gl =
      [case_tac names 
        (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns))
        (Some elim_predicate) ([],[]) ind indclause;
-      onLastHyp
+      onLastHypId
         (fun id ->
            (tclTHEN
               (apply_term (mkVar id)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1046ecbf0e..9a39b22723 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -218,7 +218,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   *)
   let invSign = named_context_val invEnv in
   let pfs = mk_pftreestate (mk_goal invSign invGoal None) in
-  let pfs = solve_pftreestate (tclTHEN intro (onLastHyp inv_op)) pfs in
+  let pfs = solve_pftreestate (tclTHEN intro (onLastHypId inv_op)) pfs in
   let (pfterm,meta_types) = extract_open_pftreestate pfs in
   let global_named_context = Global.named_context () in
   let ownSign =
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 88038a88ed..e37ffaf09f 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -278,18 +278,18 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
 	  | [None] -> intro_mustbe_force id gl
 	  | [Some th] ->
               tclTHEN (introduction id)
-                (onLastHyp (fun id -> tcc_aux (mkVar id::subst) th)) gl
+                (onLastHypId (fun id -> tcc_aux (mkVar id::subst) th)) gl
 	  | _ -> assert false
 	end
 
     | Lambda (Anonymous,_,m), _ -> (* if anon vars are allowed in evars *)
         assert (isMeta (strip_outer_cast m));
 	begin match sgp with
-	  | [None] -> tclTHEN intro (onLastHyp (fun id -> clear [id])) gl
+	  | [None] -> tclTHEN intro (onLastHypId (fun id -> clear [id])) gl
 	  | [Some th] ->
               tclTHEN
                 intro
-                (onLastHyp (fun id -> 
+                (onLastHypId (fun id -> 
                   tclTHEN
                     (clear [id])
                     (tcc_aux (mkVar (*dummy*) id::subst) th))) gl
@@ -306,7 +306,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
 	     | [None] -> introduction id
 	     | [Some th] ->
                  tclTHEN (introduction id)
-                   (onLastHyp (fun id -> tcc_aux (mkVar id::subst) th))
+                   (onLastHypId (fun id -> tcc_aux (mkVar id::subst) th))
 	     | _ -> assert false) 
 	  gl
 
@@ -317,12 +317,12 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
           (assert_tac (Name id) t1) 
 	  [(match List.hd sgp with 
 	     | None -> tclIDTAC
-	     | Some th -> onLastHyp (fun id -> tcc_aux (mkVar id::subst) th));
+	     | Some th -> onLastHypId (fun id -> tcc_aux (mkVar id::subst) th));
            (match List.tl sgp with 
 	     | [] -> refine (subst1 (mkVar id) c2)  (* a complete proof *)
 	     | [None] -> tclIDTAC                   (* a meta *)
 	     | [Some th] ->                         (* a partial proof *)
-                 onLastHyp (fun id -> tcc_aux (mkVar id::subst) th)
+                 onLastHypId (fun id -> tcc_aux (mkVar id::subst) th)
              | _ -> assert false)]
           gl
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 3cef0ef2ef..63f7507a57 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -30,32 +30,29 @@ open Evar_refiner
 open Genarg
 open Tacexpr
 
-(******************************************)
-(*         Basic Tacticals                *)
-(******************************************)
-
-(*************************************************)
-(* Tacticals re-exported from the Refiner module.*)
-(*************************************************)
-
-let tclNORMEVAR      = tclNORMEVAR
-let tclIDTAC         = tclIDTAC
-let tclIDTAC_MESSAGE = tclIDTAC_MESSAGE
-let tclORELSE0       = tclORELSE0
-let tclORELSE        = tclORELSE
-let tclTHEN          = tclTHEN
-let tclTHENLIST      = tclTHENLIST
-let tclTHEN_i        = tclTHEN_i
-let tclTHENFIRST     = tclTHENFIRST
-let tclTHENLAST      = tclTHENLAST
-let tclTHENS         = tclTHENS
+(************************************************************************)
+(* Tacticals re-exported from the Refiner module                        *)
+(************************************************************************)
+
+let tclNORMEVAR      = Refiner.tclNORMEVAR
+let tclIDTAC         = Refiner.tclIDTAC
+let tclIDTAC_MESSAGE = Refiner.tclIDTAC_MESSAGE
+let tclORELSE0       = Refiner.tclORELSE0
+let tclORELSE        = Refiner.tclORELSE
+let tclTHEN          = Refiner.tclTHEN
+let tclTHENLIST      = Refiner.tclTHENLIST
+let tclMAP           = Refiner.tclMAP
+let tclTHEN_i        = Refiner.tclTHEN_i
+let tclTHENFIRST     = Refiner.tclTHENFIRST
+let tclTHENLAST      = Refiner.tclTHENLAST
+let tclTHENS         = Refiner.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 tclREPEAT_MAIN   = Refiner.tclREPEAT_MAIN
 let tclFIRST         = Refiner.tclFIRST
 let tclSOLVE         = Refiner.tclSOLVE
 let tclTRY           = Refiner.tclTRY
@@ -67,41 +64,54 @@ let tclDO            = Refiner.tclDO
 let tclPROGRESS      = Refiner.tclPROGRESS
 let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
 let tclNOTSAMEGOAL   = Refiner.tclNOTSAMEGOAL
-let tclTHENTRY       = tclTHENTRY
-let tclIFTHENELSE    = tclIFTHENELSE
-let tclIFTHENSELSE   = tclIFTHENSELSE
-let tclIFTHENSVELSE   = tclIFTHENSVELSE
-let tclIFTHENTRYELSEMUST = tclIFTHENTRYELSEMUST
+let tclTHENTRY       = Refiner.tclTHENTRY
+let tclIFTHENELSE    = Refiner.tclIFTHENELSE
+let tclIFTHENSELSE   = Refiner.tclIFTHENSELSE
+let tclIFTHENSVELSE   = Refiner.tclIFTHENSVELSE
+let tclIFTHENTRYELSEMUST = Refiner.tclIFTHENTRYELSEMUST
+
+(* Synonyms *)
+
+let tclTHENSEQ       = tclTHENLIST
+
+(************************************************************************)
+(* Tacticals applying on hypotheses                                     *)
+(************************************************************************)
 
-let unTAC            = unTAC
+let nthDecl m gl =
+  try List.nth (pf_hyps gl) (m-1) 
+  with Failure _ -> error "No such assumption."
 
-(* [rclTHENSEQ [t1;..;tn] is equivalent to t1;..;tn *)
-let tclTHENSEQ = tclTHENLIST
+let nthHypId m gl = pi1 (nthDecl m gl)
+let nthHyp m gl   = mkVar (nthHypId m gl)
 
-(* map_tactical f [x1..xn] = (f x1);(f x2);...(f xn) *)
-(* tclMAP f [x1..xn] = (f x1);(f x2);...(f xn) *)
-let tclMAP tacfun l = 
-  List.fold_right (fun x -> (tclTHEN (tacfun x))) l tclIDTAC
+let lastDecl gl   = nthDecl 1 gl
+let lastHypId gl  = nthHypId 1 gl
+let lastHyp gl    = nthHyp 1 gl
 
-(* apply a tactic to the nth element of the signature  *)
+let nLastDecls n gl =
+  try list_firstn n (pf_hyps gl)
+  with Failure _ -> error "Not enough hypotheses in the goal."
 
-let tclNTH_HYP m (tac : constr->tactic) gl =
-  tac (try mkVar(let (id,_,_) = List.nth (pf_hyps gl) (m-1) in id) 
-       with Failure _ -> error "No such assumption.") gl
+let nLastHypsId n gl = List.map pi1 (nLastDecls n gl)
+let nLastHyps n gl   = List.map mkVar (nLastHypsId n gl)
 
-let tclNTH_DECL m tac gl =
-  tac (try List.nth (pf_hyps gl) (m-1) 
-       with Failure _ -> error "No such assumption.") gl
+let onNthDecl m tac gl  = tac (nthDecl m gl) gl
+let onNthHypId m tac gl = tac (nthHypId m gl) gl
+let onNthHyp m tac gl   = tac (nthHyp m gl) gl
 
-(* apply a tactic to the last element of the signature  *)
+let onLastDecl  = onNthDecl 1
+let onLastHypId = onNthHypId 1
+let onLastHyp   = onNthHyp 1
 
-let tclLAST_HYP = tclNTH_HYP 1
+let onHyps find tac gl = tac (find gl) gl
 
-let tclLAST_DECL = tclNTH_DECL 1
+let onNLastDecls n tac  = onHyps (nLastDecls n) tac
+let onNLastHypsId n tac = onHyps (nLastHypsId n) tac
+let onNLastHyps n tac   = onHyps (nLastHyps n) tac
 
-let tclLAST_NHYPS n tac gl =
-  tac (try list_firstn n (pf_ids_of_hyps gl)
-       with Failure _ -> error "No such assumptions.") gl
+let afterHyp id gl =
+  fst (list_split_when (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
 
 let tclTRY_sign (tac : constr->tactic) sign gl =
   let rec arec = function
@@ -147,7 +157,6 @@ let simple_clause_list_of cl gls =
 	List.map (fun h -> Some h) l in
   if cl.concl_occs = all_occurrences_expr then None::hyps else hyps
 
-
 (* OR-branch *)
 let tryClauses tac cl gls = 
   let rec firstrec = function
@@ -168,88 +177,12 @@ let onClausesLR tac cl gls =
   let hyps = simple_clause_list_of cl gls in
   tclMAP tac (List.rev hyps) gls
 
-(* A clause corresponding to the |n|-th hypothesis or None *)
-
-let nth_clause n gl =
-  if n = 0 then 
-    onConcl
-  else if n < 0 then 
-    let id = List.nth (List.rev (pf_ids_of_hyps gl)) (-n-1) in 
-    onHyp id
-  else 
-    let id = List.nth (pf_ids_of_hyps gl) (n-1) in 
-    onHyp id
-
-(* Gets the conclusion or the type of a given hypothesis *)
-
-let clause_type cls gl =
-  match simple_clause_of cls with
-    | None    -> pf_concl gl
-    | Some ((_,id),_) -> pf_get_hyp_typ gl id
-
-(* Functions concerning matching of clausal environments *)
-
-let pf_is_matching gls pat n =
-  is_matching_conv (pf_env gls) (project gls) pat n
-
-let pf_matches gls pat n =
-  matches_conv (pf_env gls) (project gls) pat n
-
-(* [OnCL clausefinder clausetac]
- * executes the clausefinder to find the clauses, and then executes the
- * clausetac on the clause so obtained. *)
-
-let onCL cfind cltac gl = cltac (cfind gl) gl
-
-
-(* [OnHyps hypsfinder hypstac]
- * idem [OnCL] but only for hypotheses, not for conclusion *)
-
-let onHyps find tac gl = tac (find gl) gl
-
-
-
-(* Create a clause list with all the hypotheses from the context, occuring
-   after id *)
-
-let afterHyp id gl =
-  fst (list_split_when (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
-    
-
-(* Create a singleton clause list with the last hypothesis from then context *)
-
-let lastHyp gl = List.hd (pf_ids_of_hyps gl)
-
-
-(* Create a clause list with the n last hypothesis from then context *)
-
-let nLastHyps n gl =
-  try list_firstn n (pf_hyps gl)
-  with Failure "firstn" -> error "Not enough hypotheses in the goal."
-
-
-let onClause t cls gl  = t cls gl
 let tryAllClauses  tac = tryClauses tac allClauses
 let onAllClauses   tac = onClauses tac allClauses
 let onAllClausesLR tac = onClausesLR tac allClauses
-let onNthLastHyp n tac gls = tac (nth_clause n gls) gls
 
 let tryAllHyps     tac =
   tryClauses (function Some((_,id),_) -> tac id | _ -> assert false) allHyps
-let onNLastHyps n  tac     = onHyps (nLastHyps n) (tclMAP tac)
-let onLastHyp      tac gls = tac (lastHyp gls) gls
-
-let clauseTacThen tac continuation =
-  (fun cls -> (tclTHEN (tac cls) continuation))
-
-let if_tac pred tac1 tac2 gl =
-  if pred gl then tac1 gl else tac2 gl
-
-let ifOnClause pred tac1 tac2 cls gl =
-  if pred (cls,clause_type cls gl) then
-    tac1 cls gl
-  else 
-    tac2 cls gl
 
 let ifOnHyp pred tac1 tac2 id gl =
   if pred (id,pf_get_hyp_typ gl id) then
@@ -257,9 +190,9 @@ let ifOnHyp pred tac1 tac2 id gl =
   else 
     tac2 id gl
 
-(***************************************)
-(*         Elimination Tacticals       *)
-(***************************************)
+(************************************************************************)
+(* Elimination Tacticals                                                *)
+(************************************************************************)
 
 (* The following tacticals allow to apply a tactic to the
    branches generated by the application of an elimination
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 7f2c366f7d..107510a918 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -56,13 +56,8 @@ 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 tclNTH_DECL      : int -> (named_declaration -> tactic) -> tactic
 val tclMAP           : ('a -> tactic) -> 'a list -> tactic
-val tclLAST_HYP      : (constr -> tactic) -> tactic
-val tclLAST_DECL     : (named_declaration -> tactic) -> tactic
-val tclLAST_NHYPS    : int -> (identifier list -> tactic) -> tactic
+
 val tclTRY_sign      : (constr -> tactic) -> named_context -> tactic
 val tclTRY_HYPS      : (constr -> tactic) -> tactic
 
@@ -72,51 +67,51 @@ val tclIFTHENSVELSE  : tactic -> tactic array -> tactic -> tactic
 
 val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
 
-val unTAC            : tactic -> goal sigma -> proof_tree sigma
+(*s Tacticals applying to hypotheses *)
+
+val onNthHypId       : int -> (identifier -> tactic) -> tactic
+val onNthHyp         : int -> (constr -> tactic) -> tactic
+val onNthDecl        : int -> (named_declaration -> tactic) -> tactic
+val onLastHypId      : (identifier -> tactic) -> tactic
+val onLastHyp        : (constr -> tactic) -> tactic
+val onLastDecl       : (named_declaration -> tactic) -> tactic
+val onNLastHypsId    : int -> (identifier list -> tactic) -> tactic
+val onNLastHyps      : int -> (constr list -> tactic) -> tactic
+val onNLastDecls     : int -> (named_context -> tactic) -> tactic
+
+val lastHypId   : goal sigma -> identifier
+val lastHyp     : goal sigma -> constr
+val lastDecl    : goal sigma -> named_declaration
+val nLastHypsId : int -> goal sigma -> identifier list
+val nLastHyps   : int -> goal sigma -> constr list
+val nLastDecls  : int -> goal sigma -> named_context
+
+val afterHyp    : identifier -> goal sigma -> named_context
+
+val ifOnHyp     : (identifier * types -> bool) ->
+                  (identifier -> tactic) -> (identifier -> tactic) ->
+		   identifier -> tactic
 
-(*s Clause tacticals. *)
+val onHyps      : (goal sigma -> named_context) -> 
+                  (named_context -> tactic) -> tactic
+
+(* Tacticals applying to hypotheses or goal *)
 
 type simple_clause = identifier gsimple_clause
 type clause = identifier gclause
 
-val allClauses : 'a gclause
-val allHyps : clause
-val onHyp : identifier -> clause
-val onConcl : 'a gclause
+val allClauses : clause
+val allHyps    : clause
+val onHyp      : identifier -> clause
+val onConcl    : clause
 
-val nth_clause  : int -> goal sigma -> clause
-val clause_type : clause -> goal sigma -> constr
 val simple_clause_list_of : clause -> goal sigma -> simple_clause list
 
-val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map
-val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
-
-val afterHyp   : identifier -> goal sigma -> named_context
-val lastHyp    : goal sigma -> identifier
-val nLastHyps  : int -> goal sigma -> named_context
-
-val onCL           : (goal sigma -> clause) -> 
-                     (clause -> tactic) -> tactic
+val tryAllHyps     : (identifier -> tactic) -> tactic
 val tryAllClauses  : (simple_clause -> tactic) -> tactic
 val onAllClauses   : (simple_clause -> tactic) -> tactic
-val onClause       : (clause -> tactic) -> clause -> tactic
 val onClauses      : (simple_clause -> tactic) -> clause -> tactic
 val onAllClausesLR : (simple_clause -> tactic) -> tactic
-val onNthLastHyp   : int -> (clause -> tactic) -> tactic
-val clauseTacThen  : (clause -> tactic) -> tactic -> clause -> tactic
-val if_tac         : (goal sigma -> bool) -> tactic -> (tactic) -> tactic
-val ifOnClause     : 
-  (clause * types -> bool) ->
-    (clause -> tactic) -> (clause -> tactic) -> clause -> tactic
-val ifOnHyp        : 
-  (identifier * types -> bool) ->
-    (identifier -> tactic) -> (identifier -> tactic) -> identifier -> tactic
-
-val onHyps         : (goal sigma -> named_context) -> 
-                     (named_context -> tactic) -> tactic
-val tryAllHyps     : (identifier -> tactic) -> tactic
-val onNLastHyps    : int -> (named_declaration -> tactic) -> tactic
-val onLastHyp      : (identifier -> tactic) -> tactic
 
 (*s Elimination tacticals. *)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d74c9f05e0..8f8482d782 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -477,7 +477,7 @@ let intros_until_n_wored = intros_until_n_gen false
 
 let try_intros_until tac = function
   | NamedHyp id -> tclTHEN (tclTRY (intros_until_id id)) (tac id)
-  | AnonHyp n -> tclTHEN (intros_until_n n) (onLastHyp tac)
+  | AnonHyp n -> tclTHEN (intros_until_n n) (onLastHypId tac)
 
 let rec intros_move = function
   | [] -> tclIDTAC
@@ -500,7 +500,7 @@ let onInductionArg tac = function
       else
 	tac cbl
   | ElimOnAnonHyp n ->
-      tclTHEN (intros_until_n n) (tclLAST_HYP (fun c -> tac (c,NoBindings)))
+      tclTHEN (intros_until_n n) (onLastHyp (fun c -> tac (c,NoBindings)))
   | ElimOnIdent (_,id) ->
       (*Identifier apart because id can be quantified in goal and not typable*)
       tclTHEN (tclTRY (intros_until_id id)) (tac (mkVar id,NoBindings))
@@ -535,7 +535,7 @@ let resolve_classes gl =
 (**************************)
 
 let cut c gl =
-  match kind_of_term (hnf_type_of gl c) with
+  match kind_of_term (pf_hnf_type_of gl c) with
     | Sort _ ->
         let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
         let t = mkProd (Anonymous, c, pf_concl gl) in
@@ -723,7 +723,7 @@ let descend_in_conjunctions with_evars tac exit c gl =
 	  (general_elim with_evars (c,NoBindings) (elim,NoBindings))
 	  (tclTHENLIST [
 	    tclDO n intro;
-	    tclLAST_NHYPS n (fun l ->
+	    onNLastHypsId n (fun l ->
 	      tclFIRST
 		(List.map (fun id -> tclTHEN (tac (mkVar id)) (thin l)) l))])
           gl
@@ -974,7 +974,7 @@ let rec intros_clearing = function
   | (false::tl) -> tclTHEN intro (intros_clearing tl)
   | (true::tl)  ->
       tclTHENLIST
-        [ intro; onLastHyp (fun id -> clear [id]); intros_clearing tl]
+        [ intro; onLastHypId (fun id -> clear [id]); intros_clearing tl]
 
 (* Modifying/Adding an hypothesis  *)
 
@@ -1097,8 +1097,8 @@ let forward_general_multi_rewrite =
 let register_general_multi_rewrite f =
   forward_general_multi_rewrite := f
 
-let clear_last = tclLAST_HYP (fun c -> (clear [destVar c]))
-let case_last  = tclLAST_HYP simplest_case
+let clear_last = onLastHyp (fun c -> (clear [destVar c]))
+let case_last  = onLastHyp simplest_case
 
 let error_unexpected_extra_pattern loc nb pat =
   let s1,s2,s3 = match pat with
@@ -1111,7 +1111,7 @@ let error_unexpected_extra_pattern loc nb pat =
       strbrk " expected in the branch).")
 
 let intro_or_and_pattern loc b ll l' tac =
-  tclLAST_HYP (fun c gl ->
+  onLastHyp (fun c gl ->
     let ind,_ = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
     let nv = mis_constr_nargs ind in
     let bracketed = b or not (l'=[]) in
@@ -1172,7 +1172,7 @@ let rec intros_patterns b avoid thin destopt = function
   | (loc, IntroWildcard) :: l ->
       tclTHEN 
         (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true)
-        (onLastHyp (fun id ->
+        (onLastHypId (fun id ->
 	  tclORELSE
 	    (tclTHEN (clear [id]) (intros_patterns b avoid thin destopt l))
 	    (intros_patterns b avoid ((loc,id)::thin) destopt l)))
@@ -1198,7 +1198,7 @@ let rec intros_patterns b avoid thin destopt = function
   | (loc, IntroRewrite l2r) :: l ->
       tclTHEN 
         (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true)
-        (onLastHyp (fun id ->
+        (onLastHypId (fun id ->
 	  tclTHEN
 	    (rewrite_hyp l2r id)
 	    (intros_patterns b avoid thin destopt l)))
@@ -1242,7 +1242,7 @@ let allow_replace c gl = function (* A rather arbitrary condition... *)
       false
 
 let assert_as first ipat c gl =
-  match kind_of_term (hnf_type_of gl c) with
+  match kind_of_term (pf_hnf_type_of gl c) with
   | Sort s ->
       let id,tac = prepare_intros s ipat gl in
       let repl = allow_replace c gl ipat in
@@ -2813,8 +2813,8 @@ let new_destruct ev lc e idl cls = induct_destruct false ev (lc,e,idl,cls)
 (* Induction tactics *)
 
 (* This was Induction before 6.3 (induction only in quantified premisses) *)
-let raw_induct s = tclTHEN (intros_until_id s) (tclLAST_HYP simplest_elim)
-let raw_induct_nodep n = tclTHEN (intros_until_n n) (tclLAST_HYP simplest_elim)
+let raw_induct s = tclTHEN (intros_until_id s) (onLastHyp simplest_elim)
+let raw_induct_nodep n = tclTHEN (intros_until_n n) (onLastHyp simplest_elim)
 
 let simple_induct_id hyp = raw_induct hyp
 let simple_induct_nodep = raw_induct_nodep
@@ -2826,9 +2826,9 @@ let simple_induct = function
 (* Destruction tactics *)
 
 let simple_destruct_id s    =
-  (tclTHEN (intros_until_id s) (tclLAST_HYP simplest_case))
+  (tclTHEN (intros_until_id s) (onLastHyp simplest_case))
 let simple_destruct_nodep n =
-  (tclTHEN (intros_until_n n)    (tclLAST_HYP simplest_case))
+  (tclTHEN (intros_until_n n)    (onLastHyp simplest_case))
 
 let simple_destruct = function
   | NamedHyp id -> simple_destruct_id id
@@ -2990,7 +2990,7 @@ let symmetry_red allowred gl =
 	    tclTHENFIRST (cut symc)
               (tclTHENLIST 
 		[ intro;
-		  tclLAST_HYP simplest_case;
+		  onLastHyp simplest_case;
 		  one_constructor 1 NoBindings ])
 	      gl
 	end)
@@ -3071,7 +3071,7 @@ let transitivity_red allowred t gl =
 	      (tclTHENFIRST (cut eq1)
                 (tclTHENLIST
 		  [ tclDO 2 intro;
-		    tclLAST_HYP simplest_case;
+		    onLastHyp simplest_case;
 		    assumption ])) gl
         end)