Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"

now works correctly, "unfold foo at 4 in H at 3" now fails correctly,
etc.). The terminology for clauses (though I don't find the term
"clause" very intuitive after all) is mostly preserved except for
"simple_clause" which becomes a light form of "clause" instead of
being an atom of clause (what played the role of "simple_clause" is
now called "goal_location" - better names are welcome).
Main changes are in tacticals.ml and tactics.ml.



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

6 files changed, 14 insertions, 15 deletions

diff --git a/contrib/firstorder/g_ground.ml4 b/contrib/firstorder/g_ground.ml4
index 3ee1db14c9..d7c5b66ae7 100644
--- a/contrib/firstorder/g_ground.ml4
+++ b/contrib/firstorder/g_ground.ml4
@@ -89,7 +89,7 @@ let defined_connectives=lazy
    [],EvalConstRef (destConst (constant "iff"))]
 
 let normalize_evaluables=
-  onAllClauses
+  onAllHypsAndConcl
     (function 
 	 None->unfold_in_concl (Lazy.force defined_connectives)
        | Some id-> 
diff --git a/contrib/firstorder/rules.ml b/contrib/firstorder/rules.ml
index 91607ec40f..fc31ee6fc7 100644
--- a/contrib/firstorder/rules.ml
+++ b/contrib/firstorder/rules.ml
@@ -208,9 +208,8 @@ let defined_connectives=lazy
    all_occurrences,EvalConstRef (destConst (constant "iff"))]
 
 let normalize_evaluables=
-  onAllClauses
+  onAllHypsAndConcl
     (function 
 	 None->unfold_in_concl (Lazy.force defined_connectives)
-       | Some ((_,id),_)-> 
-	   unfold_in_hyp (Lazy.force defined_connectives) 
-	   ((Rawterm.all_occurrences_expr,id),InHypTypeOnly))
+       | Some id -> 
+	   unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 5c8f087156..5f8587408b 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -565,11 +565,11 @@ let rec reflexivity_with_destruct_cases g =
   in
   let eq_ind =     Coqlib.build_coq_eq () in
   let discr_inject =
-    Tacticals.onAllClauses (
+    Tacticals.onAllHypsAndConcl (
        fun sc g -> 
 	 match sc with 
 	     None -> tclIDTAC g
-	   | Some ((_,id),_) -> 
+	   | Some id -> 
 	       match kind_of_term  (pf_type_of g (mkVar id)) with 
 		 | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind -> 
 		     if Equality.discriminable (pf_env g) (project g) t1 t2 
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index aee133f6d9..a96ec6a438 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -1158,7 +1158,7 @@ let rec introduce_all_values_eq cont_tac functional termine
            simpl_iter (onHyp heq2);
            unfold_in_hyp [((true,[1]), evaluable_of_global_reference 
                              (global_of_constr functional))]
-             ((all_occurrences_expr, heq2), InHyp);
+             (heq2, InHyp);
            tclTHENS
 	     (fun gls -> 
 		let t_eq = compute_renamed_type gls (mkVar heq2) in 
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 17020c46d0..57b4d1af89 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -457,7 +457,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
   let decomp_tacs = match decomp with 
     | 0 -> [] 
     | p -> 
-	(tclTRY_sign decomp_empty_term extra_sign)
+	(tclFIRST_PROGRESS_ON decomp_empty_term extra_sign)
 	::
 	(List.map 
 	   (fun id -> tclTHEN (decomp_unary_term (mkVar id)) 
@@ -469,7 +469,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
   let intro_tac = 
     tclTHEN intro 
       (fun g' -> 
-	 let (hid,_,htyp as d) = pf_last_hyp g' in
+	 let (hid,_,htyp) = pf_last_hyp g' in
 	 let hintl = 
 	   try 
 	     [make_apply_entry (pf_env g') (project g')
@@ -479,7 +479,8 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	   with Failure _ -> [] 
 	 in
          (free_try
-	  (search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d])
+	  (search_gen decomp n db_list (Hint_db.add_list hintl local_db)
+	    [mkVar hid])
 	  g'))
   in
   let rec_tacs = 
@@ -487,7 +488,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
       (fun ntac -> 
 	 tclTHEN ntac
 	   (free_try
-	    (search_gen decomp (n-1) db_list local_db empty_named_context)))
+	    (search_gen decomp (n-1) db_list local_db [])))
       (possible_resolve db_list local_db (pf_concl goal))
   in 
   tclFIRST (assumption::(decomp_tacs@(intro_tac::rec_tacs))) goal
@@ -501,7 +502,7 @@ let full_auto n gl =
   let dbnames = current_db_names () in
   let dbnames = list_subtract dbnames ["v62"] in
   let db_list = List.map searchtable_map dbnames in
-  let hyps = pf_hyps gl in
+  let hyps = List.map mkVar (pf_ids_of_hyps gl) in
   tclTRY (search n db_list (make_local_hint_db false [] gl) hyps) gl
   
 let default_full_auto gl = full_auto !default_search_depth gl
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 617ee4bed4..2888f16f1a 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -104,8 +104,7 @@ let protect_tac map =
   Tactics.reduct_option (protect_red map,DEFAULTcast) None ;;
 
 let protect_tac_in map id =
-  Tactics.reduct_option (protect_red map,DEFAULTcast)
-    (Some((all_occurrences_expr,id),InHyp));;
+  Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id,InHyp));;
 
 
 TACTIC EXTEND protect_fv