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

21 files changed, 343 insertions, 155 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
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 447bb734a7..801c0334b4 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -418,13 +418,13 @@ let pr_hyp_location pr_id = function
 
 let pr_in pp = spc () ++ hov 0 (str "in" ++ pp)
 
-let pr_simple_clause pr_id = function
+let pr_simple_hyp_clause pr_id = function
   | [] -> mt ()
   | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
 
 let pr_in_hyp_as pr_id = function
   | None -> mt ()
-  | Some (id,ipat) -> pr_simple_clause pr_id [id] ++ pr_as_ipat ipat
+  | Some (id,ipat) -> pr_simple_hyp_clause pr_id [id] ++ pr_as_ipat ipat
 
 let pr_clauses pr_id = function
   | { onhyps=None; concl_occs=occs } ->
@@ -869,11 +869,11 @@ and pr_atom1 = function
   | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
       hov 1 (pr_induction_kind k ++ spc () ++
       pr_quantified_hypothesis hyp ++
-      pr_with_inversion_names ids ++ pr_simple_clause pr_ident cl)
+      pr_with_inversion_names ids ++ pr_simple_hyp_clause pr_ident cl)
   | TacInversion (InversionUsing (c,cl),hyp) ->
       hov 1 (str "inversion" ++ spc() ++ pr_quantified_hypothesis hyp ++ 
       spc () ++ str "using" ++ spc () ++ pr_constr c ++ 
-      pr_simple_clause pr_ident cl)
+      pr_simple_hyp_clause pr_ident cl)
 
 in
 
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 5bd8060ae1..9f81ffee7f 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -92,8 +92,6 @@ and tactic_arg =
    glob_tactic_expr)
      Tacexpr.gen_tactic_arg
 
-type hyp_location = identifier Tacexpr.raw_hyp_location
-
 type ltac_call_kind = 
   | LtacNotationCall of string
   | LtacNameCall of ltac_constant
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 0bd0eaa113..5fb463da73 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -127,8 +127,6 @@ and tactic_arg =
    glob_tactic_expr)
      Tacexpr.gen_tactic_arg
 
-type hyp_location = identifier Tacexpr.raw_hyp_location
-
 type ltac_call_kind = 
   | LtacNotationCall of string
   | LtacNameCall of ltac_constant
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 2413e73ecf..6b153fa102 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -98,23 +98,22 @@ type 'id message_token =
   | MsgInt of int
   | MsgIdent of 'id
 
-type 'id gsimple_clause = ('id raw_hyp_location) option
 (* onhyps:
      [None] means *on every hypothesis*
      [Some l] means on hypothesis belonging to l *)
 type 'id gclause =
   { onhyps : 'id raw_hyp_location list option;
-    concl_occs : bool * int or_var list }
+    concl_occs : occurrences_expr }
 
 let nowhere = {onhyps=Some[]; concl_occs=no_occurrences_expr}
 
-let simple_clause_of = function
+let goal_location_of = function
 | { onhyps = Some [scl]; concl_occs = occs } when occs = no_occurrences_expr ->
       Some scl
 | { onhyps = Some []; concl_occs = occs } when occs = all_occurrences_expr ->
     None
 | _ ->
-    error "not a simple clause (one hypothesis or conclusion)"
+    error "Not a simple \"in\" clause (one hypothesis or the conclusion)"
 
 type ('constr,'id) induction_clause = 
     ('constr with_bindings induction_arg list * 'constr with_bindings option * 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 1398a335af..36fe179ad1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1090,10 +1090,10 @@ let compileAutoArg contac = function
 	     ctx) g)
   | UsingTDB ->  
       (tclTHEN  
-         (Tacticals.tryAllClauses 
+         (Tacticals.tryAllHypsAndConcl 
             (function 
-               | Some ((_,id),_) -> Dhyp.h_destructHyp false id
-               | None          -> Dhyp.h_destructConcl))
+               | Some id -> Dhyp.h_destructHyp false id
+               | None    -> Dhyp.h_destructConcl))
          contac)
 
 let compileAutoArgList contac = List.map (compileAutoArg contac)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 672c3d21cc..89088c8a15 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -1029,7 +1029,7 @@ let build_new gl env sigma flags loccs hypinfo concl cstr evars =
 let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause gl =
   let concl, is_hyp = 
     match clause with
-	Some ((_, id), _) -> pf_get_hyp_typ gl id, Some id
+	Some id -> pf_get_hyp_typ gl id, Some id
       | None -> pf_concl gl, None
   in
   let cstr = 
@@ -1120,9 +1120,9 @@ let occurrences_of = function
       (true,nl)
 
 TACTIC EXTEND class_rewrite
-| [ "clrewrite" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), [])) ]
-| [ "clrewrite" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), [])) ]
-| [ "clrewrite" orient(o) open_constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o all_occurrences (Some (([],id), [])) ]
+| [ "clrewrite" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ]
+| [ "clrewrite" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ]
+| [ "clrewrite" orient(o) open_constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o all_occurrences (Some id) ]
 | [ "clrewrite" orient(o) open_constr(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) None ]
 | [ "clrewrite" orient(o) open_constr(c) ] -> [ cl_rewrite_clause c o all_occurrences None ]
 END
@@ -1130,10 +1130,10 @@ END
 
 let clsubstitute o c =
   let is_tac id = match kind_of_term (snd c) with Var id' when id' = id -> true | _ -> false in
-    Tacticals.onAllClauses 
+    Tacticals.onAllHypsAndConcl 
       (fun cl -> 
 	match cl with
-	  | Some ((_,id),_) when is_tac id -> tclIDTAC
+	  | Some id when is_tac id -> tclIDTAC
 	  | _ -> tclTRY (cl_rewrite_clause c o all_occurrences cl))
 
 TACTIC EXTEND substitute
@@ -1214,13 +1214,13 @@ TACTIC EXTEND setoid_rewrite
    [ "setoid_rewrite" orient(o) open_constr(c) ]
    -> [ cl_rewrite_clause c o all_occurrences None ]
  | [ "setoid_rewrite" orient(o) open_constr(c) "in" hyp(id) ] ->
-      [ cl_rewrite_clause c o all_occurrences (Some (([],id), []))]
+      [ cl_rewrite_clause c o all_occurrences (Some id)]
  | [ "setoid_rewrite" orient(o) open_constr(c) "at" occurrences(occ) ] ->
       [ cl_rewrite_clause c o (occurrences_of occ) None]
  | [ "setoid_rewrite" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id)] ->
-      [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), []))]
+      [ cl_rewrite_clause c o (occurrences_of occ) (Some id)]
  | [ "setoid_rewrite" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ)] ->
-      [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), []))]
+      [ cl_rewrite_clause c o (occurrences_of occ) (Some id)]
 END
 
 (* let solve_obligation lemma =  *)
@@ -1596,8 +1596,7 @@ let general_rewrite_flags = { under_lambdas = false; on_morphisms = false }
 let general_s_rewrite cl l2r occs c ~new_goals gl =
   let meta = Evarutil.new_meta() in
   let hypinfo = ref (get_hyp gl c cl l2r) in
-  let cl' = Option.map (fun id -> (([],id), [])) cl in
-    cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta occs cl' gl
+    cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta occs cl gl
 (*     if fst c = Evd.empty || fst c == project gl then tac gl *)
 (*     else *)
 (*       let evars = Evd.merge (fst c) (project gl) in *)
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index b7929b29ac..35d2e13244 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -296,11 +296,11 @@ let set_extern_interp f = forward_interp_tactic := f
 
 let applyDestructor cls discard dd gls =
   match_dpat dd.d_pat cls gls;
-  let cll = simple_clause_list_of cls gls in
+  let cll = simple_clause_of cls gls in
   let tacl =
     List.map (fun cl ->
       match cl, dd.d_code with
-        | Some ((_,id),_), (Some x, tac) -> 
+        | Some id, (Some x, tac) -> 
 	    let arg =
               ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in
             TacLetIn (false, [(dummy_loc, x), arg], tac)
@@ -311,7 +311,7 @@ let applyDestructor cls discard dd gls =
   let discard_0 =
     List.map (fun cl ->
       match (cl,dd.d_pat) with
-        | (Some ((_,id),_),HypLocation(discardable,_,_)) ->
+        | (Some id,HypLocation(discardable,_,_)) ->
             if discard & discardable then thin [id] else tclIDTAC
         | (None,ConclLocation _) -> tclIDTAC
         | _ -> error "ApplyDestructor" ) cll in
@@ -357,9 +357,9 @@ let rec search n =
     [intros;
      assumption;
      (tclTHEN  
-        (Tacticals.tryAllClauses 
+        (Tacticals.tryAllHypsAndConcl 
            (function 
-              | Some ((_,id),_) -> (dHyp id)
+              | Some id -> (dHyp id)
               | None    ->  dConcl ))
         (search (n-1)))]
     
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0ebe44197f..3af4fa171f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -623,11 +623,11 @@ let onNegatedEquality with_evars tac gls =
 
 let discrSimpleClause with_evars = function
   | None -> onNegatedEquality with_evars discrEq
-  | Some ((_,id),_) -> onEquality with_evars discrEq (mkVar id,NoBindings)
+  | Some id -> onEquality with_evars discrEq (mkVar id,NoBindings)
 
 let discr with_evars = onEquality with_evars discrEq
 
-let discrClause with_evars = onClauses (discrSimpleClause with_evars)
+let discrClause with_evars = onClause (discrSimpleClause with_evars)
 
 let discrEverywhere with_evars = 
   tclORELSE
@@ -1142,8 +1142,7 @@ let unfold_body x gl =
       | _ -> errorlabstrm "unfold_body"
           (pr_id x ++ str" is not a defined hypothesis.") in
   let aft = afterHyp x gl in
-  let hl = List.fold_right 
-    (fun (y,yval,_) cl -> ((all_occurrences_expr,y),InHyp) :: cl) aft [] in
+  let hl = List.fold_right (fun (y,yval,_) cl -> (y,InHyp) :: cl) aft [] in
   let xvar = mkVar x in
   let rfun _ _ c = replace_term xvar xval c in
   tclTHENLIST
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index c9992c36ff..60916fda4c 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -78,7 +78,7 @@ let h_let_tac b na c cl =
 let h_instantiate n c ido = 
 (Evar_tactics.instantiate n c ido)
   (* abstract_tactic (TacInstantiate (n,c,cls))
-    (Evar_refiner.instantiate n c (simple_clause_of cls)) *)
+    (Evar_refiner.instantiate n c (goal_location_of cls)) *)
 
 (* Derived basic tactics *)
 let h_simple_induction_destruct isrec h =
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 63f7507a57..1ab01ae3e0 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -74,6 +74,13 @@ let tclIFTHENTRYELSEMUST = Refiner.tclIFTHENTRYELSEMUST
 
 let tclTHENSEQ       = tclTHENLIST
 
+(* Experimental *)
+
+let rec tclFIRST_PROGRESS_ON tac = function
+  | []    -> tclFAIL 0 (str "No applicable tactic")
+  | [a]   -> tac a (* so that returned failure is the one from last item *)
+  | a::tl -> tclORELSE (tac a) (tclFIRST_PROGRESS_ON tac tl)
+
 (************************************************************************)
 (* Tacticals applying on hypotheses                                     *)
 (************************************************************************)
@@ -113,17 +120,6 @@ let onNLastHyps n tac   = onHyps (nLastHyps n) tac
 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
-    | []      -> tclFAIL 0 (str "No applicable hypothesis.")
-    | [s]     -> tac (mkVar s) (*added in order to get useful error messages *)
-    | (s::sl) -> tclORELSE (tac (mkVar s)) (arec sl) 
-  in 
-  arec (ids_of_named_context sign) gl
-
-let tclTRY_HYPS (tac : constr->tactic) gl = 
-  tclTRY_sign tac (pf_hyps gl) gl
-
 (***************************************)
 (*           Clause Tacticals          *)
 (***************************************)
@@ -136,53 +132,56 @@ let tclTRY_HYPS (tac : constr->tactic) gl =
    --Eduardo (8/8/97) 
 *)
 
-(* The type of clauses *)
+(* A [simple_clause] is a set of hypotheses, possibly extended with
+   the conclusion (conclusion is represented by None) *)
+
+type simple_clause = identifier option list
+
+(* An [clause] is the algebraic form of a
+   [concrete_clause]; it may refer to all hypotheses
+   independently of the effective contents of the current goal *)
 
-type simple_clause = identifier gsimple_clause
 type clause = identifier gclause
 
 let allClauses = { 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 =
-  { onhyps=Some[((all_occurrences_expr,id),InHyp)]; concl_occs=no_occurrences_expr }
-
-let simple_clause_list_of cl gls =
+  { onhyps=Some[((all_occurrences_expr,id),InHyp)];
+    concl_occs=no_occurrences_expr }
+
+let simple_clause_of cl gls =
+  let error_occurrences () =
+    error "This tactic does not support occurrences selection" in
+  let error_body_selection () =
+    error "This tactic does not support body selection" in
   let hyps =
     match cl.onhyps with 
     | None ->
-	let f id = Some((all_occurrences_expr,id),InHyp) in
-	List.map f (pf_ids_of_hyps gls)
+	List.map Option.make (pf_ids_of_hyps gls)
     | Some l ->
-	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
-    | []      -> tclFAIL 0 (str "no applicable hypothesis")
-    | [cls]   -> tac cls (* added in order to get a useful error message *)
-    | cls::tl -> (tclORELSE (tac cls) (firstrec tl))
-  in
-  let hyps = simple_clause_list_of cl gls in
-  firstrec hyps gls
+	List.map (fun ((occs,id),w) ->
+	  if occs <> all_occurrences_expr then error_occurrences ();
+	  if w = InHypValueOnly then error_body_selection ();
+	  Some id) l in
+  if cl.concl_occs = no_occurrences_expr then hyps
+  else
+    if cl.concl_occs <> all_occurrences_expr then error_occurrences ()
+    else None :: hyps
 
-(* AND-branch *)
-let onClauses tac cl gls = 
-  let hyps = simple_clause_list_of cl gls in
-  tclMAP tac hyps gls
+let allHypsAndConcl gl = None :: List.map Option.make (pf_ids_of_hyps gl)
 
-(* AND-branch reverse order*)
-let onClausesLR tac cl gls = 
-  let hyps = simple_clause_list_of cl gls in
-  tclMAP tac (List.rev hyps) gls
+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 tryAllClauses  tac = tryClauses tac allClauses
-let onAllClauses   tac = onClauses tac allClauses
-let onAllClausesLR tac = onClausesLR tac allClauses
+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 tryAllHypsAndConclLR tac gl =
+  tclFIRST_PROGRESS_ON tac (List.rev (allHypsAndConcl gl)) gl
 
-let tryAllHyps     tac =
-  tryClauses (function Some((_,id),_) -> tac id | _ -> assert false) allHyps
+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
 
 let ifOnHyp pred tac1 tac2 id gl =
   if pred (id,pf_get_hyp_typ gl id) then
@@ -190,6 +189,52 @@ let ifOnHyp pred tac1 tac2 id gl =
   else 
     tac2 id gl
 
+
+(************************************************************************)
+(* An intermediate form of occurrence clause that select components     *)
+(* of a definition, hypotheses and possibly the goal                    *)
+(* (used for reduction tactics)                                         *)
+(************************************************************************)
+
+(* A [hyp_location] is an hypothesis together with a position, in
+   body if any, in type or in both *)
+
+type hyp_location = identifier * hyp_location_flag
+
+(* A [goal_location] is either an hypothesis (together with a position, in
+   body if any, in type or in both) or the goal *)
+
+type goal_location = hyp_location option
+
+(************************************************************************)
+(* An intermediate structure for dealing with occurrence clauses        *)
+(************************************************************************)
+
+(* [clause_atom] refers either to an hypothesis location (i.e. an
+   hypothesis with occurrences and a position, in body if any, in type
+   or in both) or to some occurrences of the conclusion *)
+
+type clause_atom =
+  | OnHyp of identifier * occurrences_expr * hyp_location_flag
+  | OnConcl of occurrences_expr
+
+(* A [concrete_clause] is an effective collection of
+  occurrences in the hypotheses and the conclusion *)
+
+type concrete_clause = clause_atom list
+
+let concrete_clause_of cl gls =
+  let hyps =
+    match cl.onhyps with 
+    | None ->
+	let f id = OnHyp (id,all_occurrences_expr,InHyp) in
+	List.map f (pf_ids_of_hyps gls)
+    | Some l ->
+	List.map (fun ((occs,id),w) -> OnHyp (id,occs,w)) l in
+  if cl.concl_occs = no_occurrences_expr then hyps
+  else 
+    OnConcl cl.concl_occs :: hyps
+
 (************************************************************************)
 (* Elimination Tacticals                                                *)
 (************************************************************************)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 107510a918..ed92afbcb5 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -21,6 +21,8 @@ open Reduction
 open Pattern
 open Genarg
 open Tacexpr
+open Termops
+open Rawterm
 (*i*)
 
 (* Tacticals i.e. functions from tactics to tactics. *)
@@ -58,15 +60,13 @@ val tclNOTSAMEGOAL   : tactic -> tactic
 val tclTHENTRY       : tactic -> tactic -> tactic
 val tclMAP           : ('a -> tactic) -> 'a list -> tactic
 
-val tclTRY_sign      : (constr -> tactic) -> named_context -> tactic
-val tclTRY_HYPS      : (constr -> tactic) -> tactic
-
-val tclIFTHENELSE    : tactic -> tactic -> tactic -> tactic
-val tclIFTHENSELSE   : tactic -> tactic list -> tactic -> tactic
-val tclIFTHENSVELSE  : tactic -> tactic array -> tactic -> tactic
-
+val tclIFTHENELSE        : tactic -> tactic -> tactic -> tactic
+val tclIFTHENSELSE       : tactic -> tactic list -> tactic -> tactic
+val tclIFTHENSVELSE      : tactic -> tactic array -> tactic -> tactic
 val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
 
+val tclFIRST_PROGRESS_ON : ('a -> tactic) -> 'a list -> tactic
+
 (*s Tacticals applying to hypotheses *)
 
 val onNthHypId       : int -> (identifier -> tactic) -> tactic
@@ -95,23 +95,65 @@ val ifOnHyp     : (identifier * types -> bool) ->
 val onHyps      : (goal sigma -> named_context) -> 
                   (named_context -> tactic) -> tactic
 
-(* Tacticals applying to hypotheses or goal *)
+(*s Tacticals applying to goal components *)
+
+(* A [simple_clause] is a set of hypotheses, possibly extended with
+   the conclusion (conclusion is represented by None) *)
+
+type simple_clause = identifier option list
+
+(* A [clause] denotes occurrences and hypotheses in a
+   goal; in particular, it can abstractly refer to the set of
+   hypotheses independently of the effective contents of the current goal *)
 
-type simple_clause = identifier gsimple_clause
 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 simple_clause_list_of : clause -> goal sigma -> simple_clause list
+val tryAllHyps          : (identifier -> tactic) -> tactic
+val tryAllHypsAndConcl  : (identifier option -> tactic) -> tactic
+
+val onAllHyps           : (identifier -> tactic) -> tactic
+val onAllHypsAndConcl   : (identifier option -> tactic) -> tactic
+val onAllHypsAndConclLR : (identifier option -> tactic) -> tactic
+
+val onClause   : (identifier option -> tactic) -> clause -> tactic
+val onClauseLR : (identifier option -> tactic) -> clause -> tactic
+
+(*s An intermediate form of occurrence clause with no mention of occurrences *)
+
+(* A [hyp_location] is an hypothesis together with a position, in
+   body if any, in type or in both *)
+
+type hyp_location = identifier * hyp_location_flag
+
+(* A [goal_location] is either an hypothesis (together with a position, in
+   body if any, in type or in both) or the goal *)
+
+type goal_location = hyp_location option
+
+(*s A concrete view of occurrence clauses *)
+
+(* [clause_atom] refers either to an hypothesis location (i.e. an
+   hypothesis with occurrences and a position, in body if any, in type
+   or in both) or to some occurrences of the conclusion *)
+
+type clause_atom =
+  | OnHyp of identifier * occurrences_expr * hyp_location_flag
+  | OnConcl of occurrences_expr
+
+(* A [concrete_clause] is an effective collection of
+  occurrences in the hypotheses and the conclusion *)
+
+type concrete_clause = clause_atom list
 
-val tryAllHyps     : (identifier -> tactic) -> tactic
-val tryAllClauses  : (simple_clause -> tactic) -> tactic
-val onAllClauses   : (simple_clause -> tactic) -> tactic
-val onClauses      : (simple_clause -> tactic) -> clause -> tactic
-val onAllClausesLR : (simple_clause -> tactic) -> tactic
+(* This interprets an [clause] in a given [goal] context *)
+val concrete_clause_of : clause -> goal sigma -> concrete_clause
 
 (*s Elimination tacticals. *)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8f8482d782..bd81a4b437 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -187,6 +187,72 @@ let pf_reduce_decl redfun where (id,c,ty) gl =
       let ty' =	if where <> InHypValueOnly then redfun' ty else ty in
       (id,Some b',ty')
 
+(* Possibly equip a reduction with the occurrences mentioned in an
+   occurrence clause *)
+
+let error_illegal_clause () =
+  error "\"at\" clause not supported in presence of an occurrence clause."
+
+let error_illegal_non_atomic_clause () =
+  error "\"at\" clause not supported in presence of a non atomic \"in\" clause."
+
+let error_illegal_non_atomic_effective_clause () =
+  error "Unsupported in presence of a non atomic \"in\" clause."
+
+let error_occurrences_not_unsupported () =
+  error "Occurrences not supported for this reduction tactic."
+
+let bind_change_occurrences occs nbcl = function
+  | None ->
+      if nbcl > 1 && occs <> all_occurrences_expr then
+	error_illegal_non_atomic_effective_clause ()
+      else
+	None
+  | Some (occl,c) ->
+      if (nbcl > 1 || occs <> all_occurrences_expr) && occl <> all_occurrences
+      then
+	error_illegal_clause ()
+      else
+	Some (Redexpr.out_with_occurrences (occs,c))
+
+let bind_red_expr_occurrences occs nbcl redexp =
+  let has_at_clause = function
+    | Unfold l -> List.exists (fun (occl,_) -> occl <> all_occurrences_expr) l
+    | Pattern l -> List.exists (fun (occl,_) -> occl <> all_occurrences_expr) l
+    | Simpl (Some (occl,_)) -> occl <> all_occurrences_expr
+    | _ -> false in
+  if occs = all_occurrences_expr then
+    if nbcl > 1 && has_at_clause redexp then
+      error_illegal_non_atomic_clause ()
+    else
+      redexp 
+  else
+    match redexp with
+    | Unfold (_::_::_) ->
+	error_illegal_clause ()
+    | Unfold [(occl,c)] ->
+	if occl <> all_occurrences_expr then
+	  error_illegal_clause ()
+	else
+	  Unfold [(occs,c)]
+    | Pattern (_::_::_) ->
+	error_illegal_clause ()
+    | Pattern [(occl,c)] ->
+	if occl <> all_occurrences_expr then
+	  error_illegal_clause ()
+	else
+	  Pattern [(occs,c)]
+    | Simpl (Some (occl,c)) ->
+	if occl <> all_occurrences_expr then
+	  error_illegal_clause ()
+	else
+	  Simpl (Some (occs,c))
+    | Red _ | Hnf | Cbv _ | Lazy _
+    | ExtraRedExpr _ | CbvVm | Fold _ | Simpl None ->
+	error_occurrences_not_unsupported ()
+    | Unfold [] | Pattern [] ->
+	assert false
+
 (* The following two tactics apply an arbitrary
    reduction function either to the conclusion or to a 
    certain hypothesis *)
@@ -194,7 +260,7 @@ let pf_reduce_decl redfun where (id,c,ty) gl =
 let reduct_in_concl (redfun,sty) gl = 
   convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl
 
-let reduct_in_hyp redfun ((_,id),where) gl =
+let reduct_in_hyp redfun (id,where) gl =
   convert_hyp_no_check
     (pf_reduce_decl redfun where (pf_get_hyp gl id) gl) gl 
 
@@ -202,13 +268,6 @@ let reduct_option redfun = function
   | Some id -> reduct_in_hyp (fst redfun) id 
   | None    -> reduct_in_concl redfun 
 
-(* The following tactic determines whether the reduction
-   function has to be applied to the conclusion or
-   to the hypotheses. *) 
-
-let redin_combinator redfun =
-  onClauses (reduct_option redfun)
-
 (* Now we introduce different instances of the previous tacticals *)
 let change_and_check cv_pb t env sigma c =
   if is_fconv cv_pb env sigma t c then 
@@ -216,7 +275,7 @@ let change_and_check cv_pb t env sigma c =
   else 
     errorlabstrm "convert-check-hyp" (str "Not convertible.")
 
-(* Use cumulutavity only if changing the conclusion not a subterm *)
+(* Use cumulativity only if changing the conclusion not a subterm *)
 let change_on_subterm cv_pb t = function
   | None -> change_and_check cv_pb t
   | Some occl -> contextually false occl (change_and_check Reduction.CONV t) 
@@ -228,19 +287,21 @@ let change_in_hyp occl t id  =
   with_check (reduct_in_hyp (change_on_subterm Reduction.CONV t occl) id)
 
 let change_option occl t = function
-    Some id -> change_in_hyp occl t id
+  | Some id -> change_in_hyp occl t id
   | None -> change_in_concl occl t
 
-let change occl c cls =
-  (match cls, occl with
-      ({onhyps=(Some(_::_::_)|None)}
-      |{onhyps=Some(_::_);concl_occs=((false,_)|(true,_::_))}),
-      Some _ ->
-	error "No occurrences expected when changing several hypotheses."
-    | _ -> ());
-  onClauses (change_option occl c) cls
+let change chg c cls gl =
+  let cls = concrete_clause_of cls gl in
+  let nbcl = List.length cls in
+  tclMAP (function
+    | OnHyp (id,occs,where) ->
+       change_option (bind_change_occurrences occs nbcl chg) c (Some (id,where))
+    | OnConcl occs ->
+       change_option (bind_change_occurrences occs nbcl chg) c None)
+    cls gl
 
 (* Pour usage interne (le niveau User est pris en compte par reduce) *)
+let try_red_in_concl    = reduct_in_concl (try_red_product,DEFAULTcast)
 let red_in_concl        = reduct_in_concl (red_product,DEFAULTcast)
 let red_in_hyp          = reduct_in_hyp   red_product
 let red_option          = reduct_option   (red_product,DEFAULTcast)
@@ -269,11 +330,24 @@ let checking_fun = function
   | Pattern _ -> with_check
   | _ -> (fun x -> x)
 
+(* The main reduction function *)
+
+let reduction_clause redexp cl =
+  let nbcl = List.length cl in
+  List.map (function
+    | OnHyp (id,occs,where) ->
+	(Some (id,where), bind_red_expr_occurrences occs nbcl redexp)
+    | OnConcl occs ->
+	(None, bind_red_expr_occurrences occs nbcl redexp)) cl
+
 let reduce redexp cl goal =
-  let red = Redexpr.reduction_of_red_expr redexp in
+  let cl = concrete_clause_of cl goal in
+  let redexps = reduction_clause redexp cl in
+  let tac = tclMAP (fun (where,redexp) ->
+    reduct_option (Redexpr.reduction_of_red_expr redexp) where) redexps in
   match redexp with
-      (Fold _|Pattern _) -> with_check (redin_combinator red cl) goal
-    | _ -> redin_combinator red cl goal
+  | Fold _ | Pattern _ -> with_check tac goal
+  | _ -> tac goal
 
 (* Unfolding occurrences of a constant *)
 
@@ -356,8 +430,7 @@ let rec intro_gen loc name_flag move_flag force_flag gl =
     | _ -> 
 	if not force_flag then raise (RefinerError IntroNeedsProduct);
 	try
-	  tclTHEN
-	    (reduce (Red true) onConcl)
+	  tclTHEN try_red_in_concl
 	    (intro_gen loc name_flag move_flag force_flag) gl
 	with Redelimination ->
 	  user_err_loc(loc,"Intro",str "No product even after head-reduction.")
@@ -1536,7 +1609,7 @@ let unfold_body x gl =
       | _ -> errorlabstrm "unfold_body"
           (pr_id x ++ str" is not a defined hypothesis.") in
   let aft = afterHyp x gl in
-  let hl = List.fold_right (fun (y,yval,_) cl -> (([],y),InHyp) :: cl) aft [] in
+  let hl = List.fold_right (fun (y,yval,_) cl -> (y,InHyp) :: cl) aft [] in
   let xvar = mkVar x in
   let rfun _ _ c = replace_term xvar xval c in
   tclTHENLIST
@@ -2887,10 +2960,10 @@ let andE id gl =
       (str("Tactic andE expects "^(string_of_id id)^" is a conjunction."))
 
 let dAnd cls =
-  onClauses
+  onClause
     (function
       | None    -> simplest_split
-      | Some ((_,id),_) -> andE id)
+      | Some id -> andE id)
     cls
 
 let orE id gl =
@@ -2902,10 +2975,10 @@ let orE id gl =
       (str("Tactic orE expects "^(string_of_id id)^" is a disjunction."))
 
 let dorE b cls =
-  onClauses
+  onClause
     (function
-      | (Some ((_,id),_)) -> orE id
-      |  None     -> (if b then right else left) NoBindings)
+      | Some id -> orE id
+      | None    -> (if b then right else left) NoBindings)
     cls
 
 let impE id gl =
@@ -2921,10 +2994,10 @@ let impE id gl =
 	      " is a an implication."))
                         
 let dImp cls =
-  onClauses
+  onClause
     (function
       | None    -> intro
-      | Some ((_,id),_) -> impE id)
+      | Some id -> impE id)
     cls
 
 (************************************************)
@@ -3020,10 +3093,10 @@ let symmetry_in id gl =
 	  gl
 
 let intros_symmetry =
-  onClauses
+  onClause
     (function
       | None -> tclTHEN intros symmetry
-      | Some ((_,id),_) -> symmetry_in id)
+      | Some id -> symmetry_in id)
 
 (* Transitivity tactics *)
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 8765541b29..d1bcc0fdb9 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -127,35 +127,35 @@ val exact_proof      : Topconstr.constr_expr -> tactic
 type tactic_reduction = env -> evar_map -> constr -> constr
 
 val reduct_in_hyp     : tactic_reduction -> hyp_location -> tactic
-val reduct_option     : tactic_reduction * cast_kind -> simple_clause -> tactic
+val reduct_option     : tactic_reduction * cast_kind -> goal_location -> tactic
 val reduct_in_concl   : tactic_reduction * cast_kind -> tactic
 val change_in_concl   : (occurrences * constr) option -> constr -> tactic
 val change_in_hyp     : (occurrences * constr) option -> constr -> 
                         hyp_location -> tactic
 val red_in_concl      : tactic
-val red_in_hyp        : hyp_location        -> tactic
-val red_option        : simple_clause -> tactic
+val red_in_hyp        : hyp_location -> tactic
+val red_option        : goal_location -> tactic
 val hnf_in_concl      : tactic
-val hnf_in_hyp        : hyp_location        -> tactic
-val hnf_option        : simple_clause -> tactic
+val hnf_in_hyp        : hyp_location -> tactic
+val hnf_option        : goal_location -> tactic
 val simpl_in_concl    : tactic
-val simpl_in_hyp      : hyp_location        -> tactic
-val simpl_option      : simple_clause -> tactic
+val simpl_in_hyp      : hyp_location -> tactic
+val simpl_option      : goal_location -> tactic
 val normalise_in_concl : tactic
-val normalise_in_hyp  : hyp_location        -> tactic
-val normalise_option  : simple_clause -> tactic
+val normalise_in_hyp  : hyp_location -> tactic
+val normalise_option  : goal_location -> tactic
 val normalise_vm_in_concl : tactic
 val unfold_in_concl   :
   (occurrences * evaluable_global_reference) list -> tactic
 val unfold_in_hyp     : 
   (occurrences * evaluable_global_reference) list -> hyp_location -> tactic
 val unfold_option     : 
-  (occurrences * evaluable_global_reference) list -> simple_clause
+  (occurrences * evaluable_global_reference) list -> goal_location
     -> tactic
 val change            :
   (occurrences * constr) option -> constr -> clause -> tactic
 val pattern_option    : 
-  (occurrences * constr) list -> simple_clause -> tactic
+  (occurrences * constr) list -> goal_location -> tactic
 val reduce            : red_expr -> clause -> tactic
 val unfold_constr     : global_reference -> tactic
 
diff --git a/test-suite/success/pattern.v b/test-suite/success/pattern.v
index 28d0bd556d..23e6f8e359 100644
--- a/test-suite/success/pattern.v
+++ b/test-suite/success/pattern.v
@@ -5,3 +5,40 @@
 
 Goal (id true,id false)=(id true,id true).
 generalize bool at 2 4 6 8 10 as B, true at 3 as tt, false as ff.
+Abort.
+
+(* Check use of occurrences in hypotheses for a reduction tactic such
+   as pattern *)
+
+(* Did not work in 8.2 *)
+Goal 0=0->True.
+intro H.
+pattern 0 in H at 2.
+set (f n := 0 = n) in H.  (* check pattern worked correctly *)
+Abort.
+
+(* Syntactic variant which was working in 8.2 *)
+Goal 0=0->True.
+intro H.
+pattern 0 at 2 in H.
+set (f n := 0 = n) in H.  (* check pattern worked correctly *)
+Abort.
+
+(* Ambiguous occurrence selection *)
+Goal 0=0->True.
+intro H.
+pattern 0 at 1 in H at 2 || exact I.  (* check pattern fails *)
+Qed.
+
+(* Ambiguous occurrence selection *)
+Goal 0=1->True.
+intro H.
+pattern 0, 1 in H at 1 2 || exact I.  (* check pattern fails *)
+Qed.
+
+(* Occurrence selection shared over hypotheses is difficult to advocate and
+   hence no longer allowed *)
+Goal 0=1->1=0->True.
+intros H1 H2.
+pattern 0 at 1, 1 in H1, H2 || exact I.  (* check pattern fails *)
+Qed.
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index a17ea69fed..66d02278c3 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -529,8 +529,7 @@ let compute_bl_tact ind lnamesparrec nparrec  =
                      tclTRY ( 
                       tclORELSE reflexivity (Equality.discr_tac false None)
                      );
-                     simpl_in_hyp
-		       ((Rawterm.all_occurrences_expr,freshz),InHyp);
+                     simpl_in_hyp (freshz,InHyp);
 (*
 repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
 *)