Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)

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

7 files changed, 24 insertions, 23 deletions

diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4
index a79b46d96b..28fec2e981 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/contrib/funind/g_indfun.ml4
@@ -356,7 +356,7 @@ let mkEq typ c1 c2 =
 let poseq_unsafe idunsafe cstr gl =
   let typ = Tacmach.pf_type_of gl cstr in
   tclTHEN
-    (Tactics.letin_tac None (Name idunsafe) cstr None allClauses)
+    (Tactics.letin_tac None (Name idunsafe) cstr None allHypsAndConcl)
     (tclTHENFIRST 
       (Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr)) 
       Tactics.reflexivity)
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index a78746d293..348a17b11b 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -111,7 +111,7 @@ let functional_induction with_clean c princl pat =
 	in
 	Tacticals.tclTHEN
 	  (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst [id])) idl )
-	  (Hiddentac.h_reduce flag Tacticals.allClauses)	
+	  (Hiddentac.h_reduce flag Tacticals.allHypsAndConcl)	
 	  g
       else Tacticals.tclIDTAC g 
 	
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index b236f04d75..5aadfa5920 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -11,6 +11,8 @@ tclNTH_DECL -> onNthDecl
 tclNTH_HYP -> onNthHyp
 onLastHyp -> onLastHypId
 onNLastHyps -> onNLastDecls
+onClauses -> onClause
+allClauses -> allHypsAndConcl
 
 + removal of various unused combinators on type "clause"
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 1ab01ae3e0..fa23cfb857 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -143,7 +143,7 @@ type simple_clause = identifier option list
 
 type clause = identifier gclause
 
-let allClauses = { onhyps=None; concl_occs=all_occurrences_expr }
+let allHypsAndConcl = { onhyps=None; concl_occs=all_occurrences_expr }
 let allHyps = { onhyps=None; concl_occs=no_occurrences_expr }
 let onConcl = { onhyps=Some[]; concl_occs=all_occurrences_expr }
 let onHyp id =
@@ -169,16 +169,16 @@ let simple_clause_of cl gls =
     if cl.concl_occs <> all_occurrences_expr then error_occurrences ()
     else None :: hyps
 
-let allHypsAndConcl gl = None :: List.map Option.make (pf_ids_of_hyps gl)
+let fullGoal gl = None :: List.map Option.make (pf_ids_of_hyps gl)
 
 let onAllHyps tac gl = tclMAP tac (pf_ids_of_hyps gl) gl
-let onAllHypsAndConcl tac gl = tclMAP tac (allHypsAndConcl gl) gl
-let onAllHypsAndConclLR tac gl = tclMAP tac (List.rev (allHypsAndConcl gl)) gl
+let onAllHypsAndConcl tac gl = tclMAP tac (fullGoal gl) gl
+let onAllHypsAndConclLR tac gl = tclMAP tac (List.rev (fullGoal gl)) gl
 
 let tryAllHyps tac gl = tclFIRST_PROGRESS_ON tac (pf_ids_of_hyps gl) gl
-let tryAllHypsAndConcl tac gl = tclFIRST_PROGRESS_ON tac (allHypsAndConcl gl) gl
+let tryAllHypsAndConcl tac gl = tclFIRST_PROGRESS_ON tac (fullGoal gl) gl
 let tryAllHypsAndConclLR tac gl =
-  tclFIRST_PROGRESS_ON tac (List.rev (allHypsAndConcl gl)) gl
+  tclFIRST_PROGRESS_ON tac (List.rev (fullGoal gl)) gl
 
 let onClause tac cl gls = tclMAP tac (simple_clause_of cl gls) gls
 let onClauseLR tac cl gls = tclMAP tac (List.rev (simple_clause_of cl gls)) gls
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index ed92afbcb5..fe6dd2d64a 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -110,10 +110,10 @@ type clause = identifier gclause
 
 val simple_clause_of : clause -> goal sigma -> simple_clause
 
-val allClauses : clause
-val allHyps    : clause
-val onHyp      : identifier -> clause
-val onConcl    : clause
+val allHypsAndConcl : clause
+val allHyps         : clause
+val onHyp           : identifier -> clause
+val onConcl         : clause
 
 val tryAllHyps          : (identifier -> tactic) -> tactic
 val tryAllHypsAndConcl  : (identifier option -> tactic) -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index bd81a4b437..83c58ee807 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1213,15 +1213,15 @@ let rewrite_hyp l2r id gl =
   match match_with_equality_type t with
   | Some (hdcncl,[_;lhs;rhs]) ->
       if l2r & isVar lhs & not (occur_var (pf_env gl) (destVar lhs) rhs) then
-	tclTHEN (rew_on l2r allClauses) (clear_var_and_eq lhs) gl
+	tclTHEN (rew_on l2r allHypsAndConcl) (clear_var_and_eq lhs) gl
       else if not l2r & isVar rhs & not (occur_var (pf_env gl) (destVar rhs) lhs) then
-	tclTHEN (rew_on l2r allClauses) (clear_var_and_eq rhs) gl
+	tclTHEN (rew_on l2r allHypsAndConcl) (clear_var_and_eq rhs) gl
       else
 	tclTHEN (rew_on l2r onConcl) (tclTRY (clear [id])) gl
   | Some (hdcncl,[c]) ->
       let l2r = not l2r in (* equality of the form eq_true *)
       if isVar c then
-	tclTHEN (rew_on l2r allClauses) (clear_var_and_eq c) gl
+	tclTHEN (rew_on l2r allHypsAndConcl) (clear_var_and_eq c) gl
       else
 	tclTHEN (rew_on l2r onConcl) (tclTRY (clear [id])) gl
   | _ ->
@@ -1300,7 +1300,7 @@ let prepare_intros s ipat gl = match ipat with
   | IntroWildcard -> let id = make_id s gl in id, clear_wildcards [dloc,id]
   | IntroRewrite l2r -> 
       let id = make_id s gl in
-      id, !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allClauses
+      id, !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allHypsAndConcl
   | IntroOrAndPattern ll -> make_id s gl, 
       intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move)
 
@@ -1330,7 +1330,7 @@ let assert_tac na = assert_as true (ipat_of_name na)
 
 let as_tac id ipat = match ipat with
   | Some (loc,IntroRewrite l2r) -> 
-      !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allClauses
+      !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allHypsAndConcl
   | Some (loc,IntroOrAndPattern ll) ->
       intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move)
   | Some (loc,
@@ -1769,14 +1769,14 @@ let atomize_param_of_ind (indref,nparams) hyp0 gl =
 	| Var id ->
 	    let x = fresh_id [] id gl in
 	    tclTHEN
-	      (letin_tac None (Name x) (mkVar id) None allClauses)
+	      (letin_tac None (Name x) (mkVar id) None allHypsAndConcl)
 	      (atomize_one (i-1) ((mkVar x)::avoid)) gl
 	| _ ->
 	    let id = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c)
 		       Anonymous in
 	    let x = fresh_id [] id gl in
 	    tclTHEN
-	      (letin_tac None (Name x) c None allClauses)
+	      (letin_tac None (Name x) c None allHypsAndConcl)
 	      (atomize_one (i-1) ((mkVar x)::avoid)) gl
     else 
       tclIDTAC gl
@@ -2782,7 +2782,7 @@ let new_induct_gen isrec with_evars elim (eqname,names) (c,lbind) cls gl =
 	let with_eq = Option.map (fun eq -> (false,eq)) eqname in
 	(* TODO: if ind has predicate parameters, use JMeq instead of eq *)
 	tclTHEN
-	  (letin_tac_gen with_eq (Name id) c None (Option.default allClauses cls,false))
+	  (letin_tac_gen with_eq (Name id) c None (Option.default allHypsAndConcl cls,false))
 	  (induction_with_atomization_of_ind_arg
 	     isrec with_evars elim names (id,lbind) inhyps) gl
 
@@ -2816,7 +2816,7 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc gl =
 		let _ = newlc:=id::!newlc in
 		let _ = letids:=id::!letids in
 		tclTHEN 
-		  (letin_tac None (Name id) c None allClauses)
+		  (letin_tac None (Name id) c None allHypsAndConcl)
 		  (atomize_list newl') gl in
   tclTHENLIST 
     [
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d1bcc0fdb9..dd18aa86ac 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -150,8 +150,7 @@ val unfold_in_concl   :
 val unfold_in_hyp     : 
   (occurrences * evaluable_global_reference) list -> hyp_location -> tactic
 val unfold_option     : 
-  (occurrences * evaluable_global_reference) list -> goal_location
-    -> tactic
+  (occurrences * evaluable_global_reference) list -> goal_location -> tactic
 val change            :
   (occurrences * constr) option -> constr -> clause -> tactic
 val pattern_option    :