factorisation et generalisation des clauses

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

12 files changed, 241 insertions, 164 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index de23d854b2..f10b2100c1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -881,8 +881,8 @@ let compileAutoArg contac = function
       (tclTHEN  
          (Tacticals.tryAllClauses 
             (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/dhyp.ml b/tactics/dhyp.ml
index a124cf5df8..7f2e2dc307 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -262,16 +262,30 @@ let add_destructor_hint local na loc pat pri code =
     (inDD (local,na,{ d_pat = pat; d_pri=pri; d_code=code }))
 
 let match_dpat dp cls gls =
-  let cltyp = clause_type cls gls in
   match (cls,dp) with
-    | (Some id,HypLocation(_,hypd,concld)) ->
-        (is_matching hypd.d_typ cltyp) &
-        (is_matching hypd.d_sort (pf_type_of gls cltyp)) &
-        (is_matching concld.d_typ (pf_concl gls)) &
-        (is_matching concld.d_sort (pf_type_of gls (pf_concl gls)))
-    | (None,ConclLocation concld) ->
-        (is_matching concld.d_typ (pf_concl gls)) &
-        (is_matching concld.d_sort (pf_type_of gls (pf_concl gls)))
+    | ({onhyps=lo;onconcl=false},HypLocation(_,hypd,concld)) ->
+        let hl = match lo with
+            Some l -> l
+          | None -> List.map (fun id -> (id,[],(InHyp,ref None)))
+                     (pf_ids_of_hyps gls) in
+        if not
+          (List.for_all
+            (fun (id,_,(hl,_)) ->
+              let cltyp = pf_get_hyp_typ gls id in
+              let cl = pf_concl gls in
+              (hl=InHyp) &
+              (is_matching hypd.d_typ cltyp) &
+              (is_matching hypd.d_sort (pf_type_of gls cltyp)) &
+              (is_matching concld.d_typ cl) &
+              (is_matching concld.d_sort (pf_type_of gls cl)))
+            hl)
+        then error "No match"
+    | ({onhyps=Some[];onconcl=true},ConclLocation concld) ->
+        let cl = pf_concl gls in
+        if not
+          ((is_matching concld.d_typ cl) &
+           (is_matching concld.d_sort (pf_type_of gls cl)))
+        then error "No match"
     | _ -> error "ApplyDestructor"
 
 let forward_interp_tactic = 
@@ -280,22 +294,27 @@ let forward_interp_tactic =
 let set_extern_interp f = forward_interp_tactic := f
 
 let applyDestructor cls discard dd gls =
-  if not (match_dpat dd.d_pat cls gls) then error "No match" else
-  let tac = match cls, dd.d_code with
-    | Some id, (Some x, tac) -> 
-	let arg = ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in
-        TacLetIn ([(dummy_loc, x), None, arg], tac)
-    | None, (None, tac) -> tac
-    | _, (Some _,_) -> error "Destructor expects an hypothesis"
-    | _, (None,_) -> error "Destructor is for conclusion" in
+  match_dpat dd.d_pat cls gls;
+  let cll = simple_clause_list_of cls gls in
+  let tacl =
+    List.map (fun cl ->
+      match cl, dd.d_code with
+        | Some (id,_,_), (Some x, tac) -> 
+	    let arg =
+              ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in
+            TacLetIn ([(dummy_loc, x), None, arg], tac)
+        | None, (None, tac) -> tac
+        | _, (Some _,_) -> error "Destructor expects an hypothesis"
+        | _, (None,_) -> error "Destructor is for conclusion")
+      cll in
   let discard_0 =
-    match (cls,dd.d_pat) with
-      | (Some id,HypLocation(discardable,_,_)) ->
-          if discard & discardable then thin [id] else tclIDTAC
-      | (None,ConclLocation _) -> tclIDTAC
-       | _ -> error "ApplyDestructor" 
-  in
-  tclTHEN (!forward_interp_tactic tac) discard_0 gls
+    List.map (fun cl ->
+      match (cl,dd.d_pat) with
+        | (Some (id,_,_),HypLocation(discardable,_,_)) ->
+            if discard & discardable then thin [id] else tclIDTAC
+        | (None,ConclLocation _) -> tclIDTAC
+        | _ -> error "ApplyDestructor" ) cll in
+  tclTHEN (tclMAP !forward_interp_tactic tacl) (tclTHENLIST discard_0) gls
 
 
 (* [DHyp id gls]
@@ -305,10 +324,10 @@ let applyDestructor cls discard dd gls =
    them in order of priority. *)
 
 let destructHyp discard id gls =
-  let hyptyp = clause_type (Some id) gls in
+  let hyptyp = pf_get_hyp_typ gls id in
   let ddl = List.map snd (lookup hyptyp) in
   let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in
-  tclFIRST (List.map (applyDestructor (Some id) discard) sorted_ddl) gls
+  tclFIRST (List.map (applyDestructor (onHyp id) discard) sorted_ddl) gls
 
 let cDHyp id gls = destructHyp true id gls
 let dHyp id gls = destructHyp false id gls
@@ -325,7 +344,7 @@ let h_destructHyp b id =
 let dConcl gls =
   let ddl = List.map snd (lookup (pf_concl gls)) in
   let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in
-  tclFIRST (List.map (applyDestructor None false) sorted_ddl) gls
+  tclFIRST (List.map (applyDestructor onConcl false) sorted_ddl) gls
 
 let h_destructConcl = abstract_tactic TacDestructConcl dConcl
 
@@ -339,7 +358,7 @@ let rec search n =
      (tclTHEN  
         (Tacticals.tryAllClauses 
            (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 2649d21d4e..40f1d2255a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -420,7 +420,7 @@ let rec build_discriminator sigma env dirn c sort = function
 	 | _ -> kont subval (build_coq_False (),mkSort (Prop Null)))
 
 let gen_absurdity id gl =
-  if is_empty_type (clause_type (Some id) gl)
+  if is_empty_type (clause_type (onHyp id) gl)
   then
     simplest_elim (mkVar id) gl
   else
@@ -468,7 +468,7 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
 exception NotDiscriminable
 
 let discr id gls =
-  let eqn = pf_whd_betadeltaiota gls (clause_type (Some id) gls) in
+  let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
   let sort = pf_type_of gls (pf_concl gls) in 
   let (lbeq,(t,t1,t2)) =
     try find_eq_data_decompose eqn
@@ -507,13 +507,16 @@ let onNegatedEquality tac gls =
     errorlabstrm "extract_negated_equality_then"
       (str"The goal should negate an equality")
 
-let discrClause = function
+
+let discrSimpleClause = function
   | None -> onNegatedEquality discr
-  | Some id -> discr id
+  | Some (id,_,_) -> discr id
+
+let discrClause = onClauses discrSimpleClause
 
 let discrEverywhere = 
   tclORELSE
-    (Tacticals.tryAllClauses discrClause)
+    (Tacticals.tryAllClauses discrSimpleClause)
     (fun gls -> 
        errorlabstrm "DiscrEverywhere" (str" No discriminable equalities"))
 
@@ -521,8 +524,8 @@ let discr_tac = function
   | None -> discrEverywhere
   | Some id -> try_intros_until discr id
 
-let discrConcl gls  = discrClause None gls
-let discrHyp id gls = discrClause (Some id) gls
+let discrConcl gls  = discrClause onConcl gls
+let discrHyp id gls = discrClause (onHyp id) gls
 
 (* returns the sigma type (sigS, sigT) with the respective
     constructor depending on the sort *)
@@ -778,7 +781,7 @@ let try_delta_expand env sigma t =
    in hd position, otherwise delta expansion is not done *)
 
 let inj id gls =
-  let eqn = pf_whd_betadeltaiota gls (clause_type (Some id) gls) in
+  let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
   let (eq,(t,t1,t2))= 
     try find_eq_data_decompose eqn
     with PatternMatchingFailure ->
@@ -840,7 +843,7 @@ let injConcl gls  = injClause None gls
 let injHyp id gls = injClause (Some id) gls
 
 let decompEqThen ntac id gls =
-  let eqn = pf_whd_betadeltaiota gls (clause_type (Some id) gls) in
+  let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
   let (lbeq,(t,t1,t2))= find_eq_data_decompose eqn in
   let sort = pf_type_of gls (pf_concl gls) in 
   let sigma = project gls in
@@ -913,7 +916,7 @@ let swapEquandsInConcl gls =
   refine (applist(sym_equal,[t;e2;e1;mkMeta (Clenv.new_meta())])) gls
 
 let swapEquandsInHyp id gls =
-  ((tclTHENS (cut_replacing id (swap_equands gls (clause_type (Some id) gls)))
+  ((tclTHENS (cut_replacing id (swap_equands gls (pf_get_hyp_typ gls id)))
       ([tclIDTAC;
       	(tclTHEN (swapEquandsInConcl) (exact_no_check (mkVar id)))]))) gls
 
@@ -1048,7 +1051,7 @@ let substInConcl l2r = if l2r then substInConcl_LR else substInConcl_RL
 
 let substInHyp_LR eqn id gls =
   let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in 
-  let body = subst_term e1 (clause_type (Some id) gls) in
+  let body = subst_term e1 (pf_get_hyp_typ gls id) in
   if not (dependent (mkRel 1) body) then errorlabstrm  "SubstInHyp" (mt ());
   (tclTHENS (cut_replacing id (subst1 e2 body))
      ([tclIDTAC;
@@ -1094,13 +1097,14 @@ let substConcl_LR = substConcl true
 *)
 
 let hypSubst l2r id cls gls =
-  match cls with
+  onClauses (function
     | None -> 
-	(tclTHENS (substInConcl l2r (clause_type (Some id) gls))
-	   ([tclIDTAC; exact_no_check (mkVar id)])) gls
-    | Some hypid -> 
-	(tclTHENS (substInHyp l2r (clause_type (Some id) gls) hypid)
-	   ([tclIDTAC;exact_no_check (mkVar id)])) gls
+	(tclTHENS (substInConcl l2r (pf_get_hyp_typ gls id))
+	   ([tclIDTAC; exact_no_check (mkVar id)]))
+    | Some (hypid,_,_) -> 
+	(tclTHENS (substInHyp l2r (pf_get_hyp_typ gls id) hypid)
+	   ([tclIDTAC;exact_no_check (mkVar id)])))
+    cls gls
 
 let hypSubst_LR = hypSubst true
 
@@ -1108,7 +1112,7 @@ let hypSubst_LR = hypSubst true
  * HypSubst id.
  *  id:a=b |- (P b)
  *)
-let substHypInConcl l2r id gls = try_rewrite (hypSubst l2r id None) gls
+let substHypInConcl l2r id gls = try_rewrite (hypSubst l2r id onConcl) gls
 let substHypInConcl_LR = substHypInConcl true
 
 (* id:a=b H:(P a) |- G
@@ -1154,7 +1158,7 @@ let unfold_body x gl =
           (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,ref None)) :: cl) aft [] in
+    (fun (y,yval,_) cl -> (y,[],(InHyp,ref None)) :: cl) aft [] in
   let xvar = mkVar x in
   let rfun _ _ c = replace_term xvar xval c in
   tclTHENLIST
diff --git a/tactics/equality.mli b/tactics/equality.mli
index bc31264466..4e22d41410 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -52,8 +52,8 @@ type elimination_types =
 val necessary_elimination : sorts -> sorts -> elimination_types 
 
 val discr        : identifier -> tactic
-val discrClause  : clause -> tactic
 val discrConcl   : tactic
+val discrClause  : clause -> tactic
 val discrHyp     : identifier -> tactic
 val discrEverywhere     : tactic
 val discr_tac    : quantified_hypothesis option -> tactic
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 5dc25889b6..ebcddc71c7 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -46,8 +46,9 @@ let h_generalize cl  = abstract_tactic (TacGeneralize cl) (generalize cl)
 let h_generalize_dep c = abstract_tactic (TacGeneralizeDep c)(generalize_dep c)
 let h_let_tac id c cl =
   abstract_tactic (TacLetTac (id,c,cl)) (letin_tac true (Names.Name id) c cl)
-let h_instantiate n c ido = 
-  abstract_tactic (TacInstantiate (n,c,ido)) (Evar_refiner.instantiate n c ido)
+let h_instantiate n c cls = 
+  abstract_tactic (TacInstantiate (n,c,cls))
+    (Evar_refiner.instantiate n c (simple_clause_of cls))
 
 (* Derived basic tactics *)
 let h_simple_induction h =
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 26e05eb31d..c63bfb84e3 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -48,7 +48,7 @@ val h_true_cut        : identifier option -> constr -> tactic
 val h_generalize      : constr list -> tactic 
 val h_generalize_dep  : constr -> tactic 
 val h_forward         : bool -> name -> constr -> tactic 
-val h_let_tac         : identifier -> constr -> identifier clause_pattern -> tactic
+val h_let_tac         : identifier -> constr -> Tacticals.clause -> tactic
 val h_instantiate     : int -> constr -> Tacticals.clause -> tactic
 
 (* Derived basic tactics *)
@@ -89,9 +89,9 @@ val h_simplest_right  : tactic
 
 
 (* Conversion *)
-val h_reduce          : Tacred.red_expr -> hyp_location list -> tactic
-val h_change          : 
-  constr occurrences option -> constr -> hyp_location list -> tactic
+val h_reduce          : Tacred.red_expr -> Tacticals.clause -> tactic
+val h_change          :
+  constr occurrences option -> constr -> Tacticals.clause -> tactic
 
 (* Equivalence relations *)
 val h_reflexivity     : tactic
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 6033ffa233..fddcf4761b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -307,8 +307,8 @@ let projectAndApply thin id eqname names depids gls =
   let env = pf_env gls in
   let clearer id =
     if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC) in
-  let subst_hyp_LR id = tclTHEN (tclTRY(hypSubst_LR id None)) (clearer id) in
-  let subst_hyp_RL id = tclTHEN (tclTRY(hypSubst_RL id None)) (clearer id) in
+  let subst_hyp_LR id = tclTHEN (tclTRY(hypSubst_LR id onConcl)) (clearer id) in
+  let subst_hyp_RL id = tclTHEN (tclTRY(hypSubst_RL id onConcl)) (clearer id) in
   let substHypIfVariable tac id gls =
     let (t,t1,t2) = Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id) in
     match (kind_of_term t1, kind_of_term t2) with
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 670cc995b9..efe2e3f2c2 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -516,7 +516,8 @@ let intern_inversion_strength lf ist = function
       InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl)
 
 (* Interprets an hypothesis name *)
-let intern_hyp_location ist (id,hl) = (intern_hyp ist (skip_metaid id), hl)
+let intern_hyp_location ist (id,occs,hl) =
+  (intern_hyp ist (skip_metaid id), occs, hl)
 
 (* Reads a pattern *)
 let intern_pattern evc env lfun = function
@@ -566,6 +567,13 @@ let extract_let_names lrc =
       name::l)
     lrc []
 
+
+let clause_app f = function
+    { onhyps=None; onconcl=b;concl_occs=nl } ->
+      { onhyps=None; onconcl=b; concl_occs=nl }
+  | { onhyps=Some l; onconcl=b;concl_occs=nl } ->
+      { onhyps=Some(List.map f l); onconcl=b;concl_occs=nl}
+
 (* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *)
 let rec intern_atomic lf ist x =
   match (x:raw_atomic_tactic_expr) with 
@@ -599,12 +607,13 @@ let rec intern_atomic lf ist x =
   | TacForward (b,na,c) -> TacForward (b,intern_name lf ist na,intern_constr ist c)
   | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl)
   | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c)
-  | TacLetTac (id,c,clp) ->
+  | TacLetTac (id,c,cls) ->
       let id = intern_ident lf ist id in
-      TacLetTac (id,intern_constr ist c,intern_clause_pattern ist clp)
-  | TacInstantiate (n,c,ido) -> 
+      TacLetTac (id,intern_constr ist c,
+                 (clause_app (intern_hyp_location ist) cls))
+  | TacInstantiate (n,c,cls) -> 
       TacInstantiate (n,intern_constr ist c,
-		      (option_app (intern_hyp_or_metaid ist) ido))
+		      (clause_app (intern_hyp_location ist) cls))
 
   (* Automation tactics *)
   | TacTrivial l -> TacTrivial l
@@ -655,15 +664,15 @@ let rec intern_atomic lf ist x =
 
   (* Conversion *)
   | TacReduce (r,cl) ->
-      TacReduce (intern_redexp ist r, List.map (intern_hyp_location ist) cl)
+      TacReduce (intern_redexp ist r, clause_app (intern_hyp_location ist) cl)
   | TacChange (occl,c,cl) ->
       TacChange (option_app (intern_constr_occurrence ist) occl,
-        intern_constr ist c, List.map (intern_hyp_location ist) cl)
+        intern_constr ist c, clause_app (intern_hyp_location ist) cl)
 
   (* Equivalence relations *)
   | TacReflexivity -> TacReflexivity
   | TacSymmetry idopt -> 
-      TacSymmetry (option_app (intern_hyp_or_metaid ist) idopt)
+      TacSymmetry (clause_app (intern_hyp_location ist) idopt)
   | TacTransitivity c -> TacTransitivity (intern_constr ist c)
 
   (* Equality and inversion *)
@@ -1066,7 +1075,12 @@ let interp_evaluable ist env = function
       coerce_to_evaluable_ref env (unrec (List.assoc id ist.lfun))
 
 (* Interprets an hypothesis name *)
-let interp_hyp_location ist gl (id,hl) = (interp_hyp ist gl id,hl)
+let interp_hyp_location ist gl (id,occs,hl) = (interp_hyp ist gl id,occs,hl)
+
+let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } =
+  { onhyps=option_app(List.map (interp_hyp_location ist gl)) ol;
+    onconcl=b;
+    concl_occs=occs }
 
 let eval_opt_ident ist = option_app (eval_ident ist)
 
@@ -1598,10 +1612,10 @@ and interp_atomic ist gl = function
   | TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl)
   | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
   | TacLetTac (id,c,clp) ->
-      let clp = interp_clause_pattern ist gl clp in
+      let clp = interp_clause ist gl clp in
       h_let_tac (eval_ident ist id) (pf_interp_constr ist gl c) clp
   | TacInstantiate (n,c,ido) -> h_instantiate n (pf_interp_constr ist gl c)
-      (option_app (interp_hyp ist gl) ido)
+      (clause_app (interp_hyp_location ist gl) ido)
 
   (* Automation tactics *)
   | TacTrivial l -> Auto.h_trivial l
@@ -1658,15 +1672,14 @@ and interp_atomic ist gl = function
 
   (* Conversion *)
   | TacReduce (r,cl) ->
-      h_reduce (pf_redexp_interp ist gl r) (List.map
-               (interp_hyp_location ist gl) cl)
+      h_reduce (pf_redexp_interp ist gl r) (interp_clause ist gl cl)
   | TacChange (occl,c,cl) ->
       h_change (option_app (pf_interp_pattern ist gl) occl)
-        (pf_interp_constr ist gl c) (List.map (interp_hyp_location ist gl) cl)
+        (pf_interp_constr ist gl c) (interp_clause ist gl cl)
 
   (* Equivalence relations *)
   | TacReflexivity -> h_reflexivity
-  | TacSymmetry c -> h_symmetry (option_app (interp_hyp ist gl) c)
+  | TacSymmetry c -> h_symmetry (interp_clause ist gl c)
   | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c)
 
   (* Equality and inversion *)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 52a12a23d8..486e3c3ee4 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -98,15 +98,6 @@ let tclTRY_sign (tac : constr->tactic) sign gl =
 let tclTRY_HYPS (tac : constr->tactic) gl = 
   tclTRY_sign tac (pf_hyps gl) gl
 
-(* OR-branch *)
-let tryClauses tac = 
-  let rec firstrec = function
-    | []      -> tclFAIL 0 "no applicable hypothesis"
-    | [cls]   -> tac cls (* added in order to get a useful error message *)
-    | cls::tl -> (tclORELSE (tac cls) (firstrec tl))
-  in 
-  firstrec
-
 (***************************************)
 (*           Clause Tacticals          *)
 (***************************************)
@@ -121,26 +112,62 @@ let tryClauses tac =
 
 (* The type of clauses *)
 
-type clause = identifier option
+type simple_clause = identifier gsimple_clause
+type clause = identifier gclause
+
+let allClauses = { onhyps=None; onconcl=true; concl_occs=[] }
+let allHyps = { onhyps=None; onconcl=false; concl_occs=[] }
+let onHyp id =
+  { onhyps=Some[(id,[],(InHyp, ref None))]; onconcl=false; concl_occs=[] }
+let onConcl = { onhyps=Some[]; onconcl=true; concl_occs=[] }
+
+let simple_clause_list_of cl gls =
+  let hyps =
+    match cl.onhyps with 
+        None ->
+          List.map (fun id -> Some(id,[],(InHyp,ref None))) (pf_ids_of_hyps gls)
+      | Some l -> List.map (fun h -> Some h) l in
+  if cl.onconcl then None::hyps else hyps
+
+
+(* OR-branch *)
+let tryClauses tac cl gls = 
+  let rec firstrec = function
+    | []      -> tclFAIL 0 "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
+
+(* AND-branch *)
+let onClauses tac cl gls = 
+  let hyps = simple_clause_list_of cl gls in
+  tclMAP tac hyps gls
+
+(* AND-branch reverse order*)
+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 
-    None
+    onConcl
   else if n < 0 then 
-    let id = List.nth (pf_ids_of_hyps gl) (-n-1) in 
-    Some id
+    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 
-    Some id
+    onHyp id
 
 (* Gets the conclusion or the type of a given hypothesis *)
 
 let clause_type cls gl =
-  match cls with
+  match simple_clause_of cls with
     | None    -> pf_concl gl
-    | Some id -> pf_get_hyp_typ gl id
+    | Some (id,_,_) -> pf_get_hyp_typ gl id
 
 (* Functions concerning matching of clausal environments *)
 
@@ -153,7 +180,7 @@ let pf_matches gls pat n =
 
 (* [OnCL clausefinder clausetac]
  * executes the clausefinder to find the clauses, and then executes the
- * clausetac on the list so obtained. *)
+ * clausetac on the clause so obtained. *)
 
 let onCL cfind cltac gl = cltac (cfind gl) gl
 
@@ -164,10 +191,6 @@ let onCL cfind cltac gl = cltac (cfind gl) gl
 let onHyps find tac gl = tac (find gl) gl
 
 
-(* Create a clause list with all the hypotheses from the context *)
-
-let allHyps gl = pf_ids_of_hyps gl
-
 
 (* Create a clause list with all the hypotheses from the context, occuring
    after id *)
@@ -188,19 +211,14 @@ let nLastHyps n gl =
   with Failure "firstn" -> error "Not enough hypotheses in the goal"
 
 
-(* A clause list with the conclusion and all the hypotheses *)
-
-let allClauses gl = 
-  let ids = pf_ids_of_hyps gl in  
-  (None::(List.map in_some ids))
-
 let onClause t cls gl  = t cls gl
-let tryAllClauses  tac = onCL allClauses (tryClauses tac)
-let onAllClauses   tac = onCL allClauses (tclMAP tac)
-let onAllClausesLR tac = onCL (compose List.rev allClauses) (tclMAP tac)
+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 gls = tryClauses tac (allHyps 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
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 7ff64996b3..10208f7383 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -68,27 +68,32 @@ val unTAC            : tactic -> goal sigma -> proof_tree sigma
 
 (*s Clause tacticals. *)
 
-type clause = identifier option
+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 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 allHyps    : goal sigma -> identifier list
 val afterHyp   : identifier -> goal sigma -> named_context
 val lastHyp    : goal sigma -> identifier
 val nLastHyps  : int -> goal sigma -> named_context
 
-val allClauses : goal sigma -> clause list
-
-val onCL           : (goal sigma -> clause list) -> 
-                     (clause list -> tactic) -> tactic
-val tryAllClauses  : (clause -> tactic) -> tactic
-val onAllClauses   : (clause -> tactic) -> tactic
+val onCL           : (goal sigma -> clause) -> 
+                     (clause -> tactic) -> tactic
+val tryAllClauses  : (simple_clause -> tactic) -> tactic
+val onAllClauses   : (simple_clause -> tactic) -> tactic
 val onClause       : (clause -> tactic) -> clause -> tactic
-val onAllClausesLR : (clause -> tactic) -> 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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 54f265c85b..ee8e32d0aa 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -143,7 +143,7 @@ type tactic_reduction = env -> evar_map -> constr -> constr
 let reduct_in_concl redfun gl = 
   convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) gl
 
-let reduct_in_hyp redfun (id,(where,where')) gl =
+let reduct_in_hyp redfun (id,_,(where,where')) gl =
   let (_,c, ty) = pf_get_hyp gl id in
   let redfun' = (*under_casts*) (pf_reduce redfun gl) in
   match c with
@@ -168,10 +168,8 @@ let reduct_option redfun = function
    function has to be applied to the conclusion or
    to the hypotheses. *) 
 
-let redin_combinator redfun = function 
-  | [] ->  reduct_in_concl redfun 
-  | x  -> (tclMAP (reduct_in_hyp redfun) x)
-
+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 =
@@ -188,12 +186,17 @@ let change_on_subterm cv_pb t = function
 let change_in_concl occl t = reduct_in_concl (change_on_subterm CUMUL t occl) 
 let change_in_hyp occl t   = reduct_in_hyp (change_on_subterm CONV t occl)
 
-let change occl c = function
-  | [] -> change_in_concl occl c
-  | l  -> 
-      if List.tl l <> [] & occl <> None then
-	error "No occurrences expected when changing several hypotheses";
-      tclMAP (change_in_hyp occl c) l
+let change_option occl t = function
+    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(_::_);onconcl=true}),
+      Some _ ->
+	error "No occurrences expected when changing several hypotheses"
+    | _ -> ());
+  onClauses (change_option occl c) cls
 
 (* Pour usage interne (le niveau User est pris en compte par reduce) *)
 let red_in_concl        = reduct_in_concl red_product
@@ -277,7 +280,7 @@ let rec intro_gen name_flag move_flag force_flag gl =
 	if not force_flag then raise (RefinerError IntroNeedsProduct);
 	try
 	  tclTHEN
-	    (reduce (Red true) [])
+	    (reduce (Red true) onConcl)
 	    (intro_gen name_flag move_flag force_flag) gl
 	with Redelimination ->
 	  errorlabstrm "Intro" (str "No product even after head-reduction")
@@ -634,16 +637,21 @@ let quantify lconstr =
    the left of each x1, ...).
 *)
 
-let occurrences_of_hyp id = function
-  | None, [] -> (* Everywhere *) Some []
-  | _, occ_hyps -> try Some (List.assoc id occ_hyps) with Not_found -> None
 
-let occurrences_of_goal = function
-  | None, [] -> (* Everywhere *) Some []
-  | Some gocc as x, _ -> x
-  | None, _ -> None
 
-let everywhere (occ_ccl,occ_hyps) = (occ_ccl = None) & (occ_hyps = [])
+let occurrences_of_hyp id cls =
+  let rec hyp_occ = function
+      [] -> None
+    | (id',occs,hl)::_ when id=id' -> Some occs
+    | _::l -> hyp_occ l in
+  match cls.onhyps with
+      None -> Some []
+    | Some l -> hyp_occ l
+
+let occurrences_of_goal cls =
+  if cls.onconcl then Some cls.concl_occs else None
+
+let everywhere cls = (cls=allClauses)
 
 (*
 (* Implementation with generalisation then re-intro: introduces noise *)
@@ -749,9 +757,11 @@ let check_hypotheses_occurrences_list env (_,occl) =
     | [] -> ()
   in check [] occl
 
-let nowhere = (Some [],[])
+let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]}
 
-let forward b na c = letin_tac b na c nowhere
+(* Tactic Pose should not perform any replacement (as specified in
+   the doc), but it does in the conclusion! *) 
+let forward b na c = letin_tac b na c onConcl
 
 (********************************************************************)
 (*               Exact tactics                                      *)
@@ -1154,14 +1164,14 @@ let atomize_param_of_ind (indref,nparams) hyp0 gl =
 	| Var id ->
 	    let x = fresh_id [] id gl in
 	    tclTHEN
-	      (letin_tac true (Name x) (mkVar id) (None,[]))
+	      (letin_tac true (Name x) (mkVar id) allClauses)
 	      (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 true (Name x) c (None,[]))
+	      (letin_tac true (Name x) c allClauses)
 	      (atomize_one (i-1) ((mkVar x)::avoid)) gl
     else 
       tclIDTAC gl
@@ -1513,7 +1523,7 @@ let new_induct_gen isrec elim names c gl =
 		  Anonymous in
 	let id = fresh_id [] x gl in
 	tclTHEN
-	  (letin_tac true (Name id) c (None,[]))
+	  (letin_tac true (Name id) c allClauses)
 	  (induction_with_atomization_of_ind_arg isrec elim names id) gl
 
 let new_induct_destruct isrec c elim names = match c with
@@ -1613,10 +1623,12 @@ let andE id gl =
     errorlabstrm "andE" 
       (str("Tactic andE expects "^(string_of_id id)^" is a conjunction."))
 
-let dAnd cls gl =
-  match cls with
-    | None    -> simplest_split gl
-    | Some id -> andE id  gl
+let dAnd cls =
+  onClauses
+    (function
+      | None    -> simplest_split
+      | Some (id,_,_) -> andE id)
+    cls
 
 let orE id gl =
   let t = pf_get_hyp_typ gl id in
@@ -1626,10 +1638,12 @@ let orE id gl =
     errorlabstrm "orE" 
       (str("Tactic orE expects "^(string_of_id id)^" is a disjunction."))
 
-let dorE b cls gl =
-  match cls with 
-    | (Some id) -> orE id gl 
-    |  None     -> (if b then right else left) NoBindings gl
+let dorE b cls =
+  onClauses
+    (function
+      | (Some (id,_,_)) -> orE id
+      |  None     -> (if b then right else left) NoBindings)
+    cls
 
 let impE id gl =
   let t = pf_get_hyp_typ gl id in
@@ -1643,10 +1657,12 @@ let impE id gl =
       (str("Tactic impE expects "^(string_of_id id)^
 	      " is a an implication."))
                         
-let dImp cls gl =
-  match cls with
-    | None    -> intro gl
-    | Some id -> impE id gl
+let dImp cls =
+  onClauses
+    (function
+      | None    -> intro
+      | Some (id,_,_) -> impE id)
+    cls
 
 (************************************************)
 (*  Tactics related with logic connectives      *)
@@ -1708,9 +1724,11 @@ let symmetry_in id gl =
             tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
 	  gl
 
-let intros_symmetry = function
-  | None -> tclTHEN intros symmetry
-  | Some id -> symmetry_in id
+let intros_symmetry =
+  onClauses
+    (function
+      | None -> tclTHEN intros symmetry
+      | Some (id,_,_) -> symmetry_in id)
 
 (* Transitivity tactics *)
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 820c20d375..90cb174839 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -108,35 +108,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 -> hyp_location option -> tactic
+val reduct_option     : tactic_reduction -> simple_clause -> tactic
 val reduct_in_concl   : tactic_reduction -> tactic
 val change_in_concl   : constr occurrences option -> constr -> tactic
 val change_in_hyp     : constr occurrences option -> constr -> hyp_location ->
   tactic
 val red_in_concl      : tactic
 val red_in_hyp        : hyp_location        -> tactic
-val red_option        : hyp_location option -> tactic
+val red_option        : simple_clause -> tactic
 val hnf_in_concl      : tactic
 val hnf_in_hyp        : hyp_location        -> tactic
-val hnf_option        : hyp_location option -> tactic
+val hnf_option        : simple_clause -> tactic
 val simpl_in_concl    : tactic
 val simpl_in_hyp      : hyp_location        -> tactic
-val simpl_option      : hyp_location option -> tactic
+val simpl_option      : simple_clause -> tactic
 val normalise_in_concl: tactic
 val normalise_in_hyp  : hyp_location        -> tactic
-val normalise_option  : hyp_location option -> tactic
+val normalise_option  : simple_clause -> tactic
 val unfold_in_concl   : (int list * evaluable_global_reference) list -> tactic
 val unfold_in_hyp     : 
   (int list * evaluable_global_reference) list -> hyp_location -> tactic
 val unfold_option     : 
-  (int list * evaluable_global_reference) list -> hyp_location option
+  (int list * evaluable_global_reference) list -> simple_clause
     -> tactic
-val reduce            : red_expr -> hyp_location list -> tactic
+val reduce            : red_expr -> clause -> tactic
 val change            :
-  constr occurrences option -> constr -> hyp_location list -> tactic
+  constr occurrences option -> constr -> clause -> tactic
 
 val unfold_constr     : global_reference -> tactic
-val pattern_option  : (int list * constr) list -> hyp_location option -> tactic
+val pattern_option  : (int list * constr) list -> simple_clause -> tactic
 
 (*s Modification of the local context. *)
 
@@ -233,8 +233,7 @@ val cut_replacing               : identifier -> constr -> tactic
 val cut_in_parallel             : constr list -> tactic
 
 val true_cut                    : identifier option -> constr -> tactic
-val letin_tac                   : bool -> name -> constr -> 
-                                  identifier clause_pattern -> tactic
+val letin_tac                   : bool -> name -> constr -> clause -> tactic
 val forward                     : bool -> name -> constr -> tactic
 val generalize                  : constr list -> tactic
 val generalize_dep              : constr  -> tactic