Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

21 files changed, 307 insertions, 216 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index d5e5e556..7c1c375b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: auto.ml 7937 2006-01-28 19:58:11Z herbelin $ *)
+(* $Id: auto.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
 
 open Pp
 open Util
@@ -778,7 +778,7 @@ let gen_auto n lems dbnames =
   | None -> full_auto n lems
   | Some l -> auto n lems l
 
-let inj_or_var = option_app (fun n -> Genarg.ArgArg n)
+let inj_or_var = option_map (fun n -> ArgArg n)
 
 let h_auto n lems l =
   Refiner.abstract_tactic (TacAuto (inj_or_var n,lems,l)) (gen_auto n lems l)
@@ -849,7 +849,7 @@ let compileAutoArg contac = function
       (tclTHEN  
          (Tacticals.tryAllClauses 
             (function 
-               | Some (id,_,_) -> Dhyp.h_destructHyp false id
+               | Some ((_,id),_) -> Dhyp.h_destructHyp false id
                | None          -> Dhyp.h_destructConcl))
          contac)
 
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 511e0950..f82b1f82 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: dhyp.ml 7732 2005-12-26 13:51:24Z herbelin $ *)
+(* $Id: dhyp.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
 
 (* Chet's comments about this tactic :
  
@@ -265,10 +265,10 @@ let match_dpat dp cls gls =
     | ({onhyps=lo;onconcl=false},HypLocation(_,hypd,concld)) ->
         let hl = match lo with
             Some l -> l
-          | None -> List.map (fun id -> (id,[],InHyp)) (pf_ids_of_hyps gls) in
+          | None -> List.map (fun id -> (([],id),InHyp)) (pf_ids_of_hyps gls) in
         if not
           (List.for_all
-            (fun (id,_,hl) ->
+            (fun ((_,id),hl) ->
               let cltyp = pf_get_hyp_typ gls id in
               let cl = pf_concl gls in
               (hl=InHyp) &
@@ -297,7 +297,7 @@ let applyDestructor cls discard dd gls =
   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 ([(dummy_loc, x), None, arg], tac)
@@ -308,7 +308,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
@@ -356,7 +356,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/eauto.ml4 b/tactics/eauto.ml4
index 457f8318..32abc347 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: eauto.ml4 7991 2006-02-05 22:56:16Z herbelin $ *)
+(* $Id: eauto.ml4 8878 2006-05-30 16:44:25Z herbelin $ *)
 
 open Pp
 open Util
@@ -107,7 +107,7 @@ let e_split = e_constructor_tac (Some 1) 1
 TACTIC EXTEND econstructor
   [ "econstructor" integer(n) "with" bindings(c) ] -> [ e_constructor_tac None n c ]
 | [ "econstructor" integer(n) ] -> [ e_constructor_tac None n NoBindings ]
-| [ "econstructor" tactic_opt(t) ] -> [ e_any_constructor (option_app Tacinterp.eval_tactic t) ] 
+| [ "econstructor" tactic_opt(t) ] -> [ e_any_constructor (option_map Tacinterp.eval_tactic t) ] 
       END
 
 TACTIC EXTEND eleft
@@ -149,7 +149,7 @@ let rec prolog l n gl =
 let prolog_tac l n gl =
   let n =
     match n with
-      |  Genarg.ArgArg n -> n
+      |  ArgArg n -> n
       | _ -> error "Prolog called with a non closed argument"
   in
   try (prolog l n gl)
@@ -383,12 +383,12 @@ let gen_eauto d np lems = function
 
 let make_depth = function
   | None -> !default_search_depth 
-  | Some (Genarg.ArgArg d) -> d
+  | Some (ArgArg d) -> d
   | _ -> error "EAuto called with a non closed argument"
 
 let make_dimension n = function
   | None -> (true,make_depth n)
-  | Some (Genarg.ArgArg d) -> (false,d)
+  | Some (ArgArg d) -> (false,d)
   | _ -> error "EAuto called with a non closed argument"
 
 open Genarg
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 9cbc549f..0a33164e 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -14,7 +14,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: eqdecide.ml4 8652 2006-03-22 08:27:14Z herbelin $ *)
+(* $Id: eqdecide.ml4 8780 2006-05-02 21:58:58Z letouzey $ *)
 
 open Util
 open Names
@@ -103,7 +103,7 @@ let mkGenDecideEqGoal rectype g =
 
 let eqCase tac = 
   (tclTHEN intro  
-  (tclTHEN (tclLAST_HYP Extratactics.h_rewriteLR)
+  (tclTHEN (tclLAST_HYP Equality.rewriteLR)
   (tclTHEN clear_last 
   tac)))
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index be79c348..42fc1201 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: equality.ml 8677 2006-04-02 17:05:59Z herbelin $ *)
+(* $Id: equality.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
 
 open Pp
 open Util
@@ -69,27 +69,47 @@ let elimination_sort_of_clause = function
   | None -> elimination_sort_of_goal
   | Some id -> elimination_sort_of_hyp id
 
+(* The next function decides in particular whether to try a regular 
+  rewrite or a setoid rewrite. 
+
+  Old approach was: 
+   break everything, if [eq] appears in head position 
+   then regular rewrite else try setoid rewrite
+ 
+  New approach is: 
+   if head position is a known setoid relation then setoid rewrite
+   else back to the old approach
+*)
+
 let general_rewrite_bindings_clause cls lft2rgt (c,l) gl =
   let ctype = pf_type_of gl c in 
-  let env = pf_env gl in
-  let sigma = project gl in 
-  let _,t = splay_prod env sigma ctype in
-  match match_with_equation t with
-    | None -> 
-	if l = NoBindings
-	then general_s_rewrite_clause cls lft2rgt c [] gl
-	else error "The term provided does not end with an equation" 
-    | Some (hdcncl,_) -> 
-        let hdcncls = string_of_inductive hdcncl in 
-	let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
-        let dir = if cls=None then lft2rgt else not lft2rgt in
-        let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
-        let elim =
-	  try pf_global gl (id_of_string rwr_thm)
-          with Not_found ->
-            error ("Cannot find rewrite principle "^rwr_thm)
-        in 
-	general_elim_clause cls (c,l) (elim,NoBindings) gl
+  (* A delta-reduction would be here too strong, since it would 
+     break search for a defined setoid relation in head position. *)
+  let t = snd (decompose_prod (whd_betaiotazeta ctype)) in 
+  let head = if isApp t then fst (destApp t) else t in 
+  if relation_table_mem head && l = NoBindings then 
+    general_s_rewrite_clause cls lft2rgt c [] gl
+  else 
+    (* Original code. In particular, [splay_prod] performs delta-reduction. *)
+    let env = pf_env gl in
+    let sigma = project gl in 
+    let _,t = splay_prod env sigma t in
+    match match_with_equation t with
+      | None -> 
+	  if l = NoBindings
+	  then general_s_rewrite_clause cls lft2rgt c [] gl
+	  else error "The term provided does not end with an equation" 
+      | Some (hdcncl,_) -> 
+          let hdcncls = string_of_inductive hdcncl in 
+	  let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
+          let dir = if cls=None then lft2rgt else not lft2rgt in
+          let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
+          let elim =
+	    try pf_global gl (id_of_string rwr_thm)
+            with Not_found ->
+              error ("Cannot find rewrite principle "^rwr_thm)
+          in 
+	  general_elim_clause cls (c,l) (elim,NoBindings) gl
 
 let general_rewrite_bindings = general_rewrite_bindings_clause None
 let general_rewrite l2r c = general_rewrite_bindings l2r (c,NoBindings)
@@ -99,6 +119,37 @@ let general_rewrite_bindings_in l2r id =
 let general_rewrite_in l2r id c = 
   general_rewrite_bindings_clause (Some id) l2r (c,NoBindings)
 
+
+let general_multi_rewrite l2r c cl = 
+  let rec do_hyps = function 
+    | [] -> tclIDTAC
+    | ((_,id),_) :: l -> 
+	tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l)
+  in 
+  let rec try_do_hyps = function 
+    | [] -> tclIDTAC 
+    | id :: l -> 
+	tclTHENFIRST 
+	  (tclTRY (general_rewrite_bindings_in l2r id c)) 
+	  (try_do_hyps l)
+  in 
+  if cl.concl_occs <> [] then 
+    error "The \"at\" syntax isn't available yet for the rewrite tactic"
+  else 
+    tclTHENFIRST 
+      (if cl.onconcl then general_rewrite_bindings l2r c else tclIDTAC)
+      (match cl.onhyps with 
+	 | Some l -> do_hyps l
+	 | None -> 
+	     fun gl -> 
+	       (* try to rewrite in all hypothesis 
+		  (except maybe the rewritten one) *)
+	       let ids = match kind_of_term (fst c) with 
+		 | Var id -> list_remove id (pf_ids_of_hyps gl)
+		 | _ -> pf_ids_of_hyps gl
+	       in try_do_hyps ids gl)
+
+
 (* Conditional rewriting, the success of a rewriting is related 
    to the resolution of the conditions by a given tactic *)
 
@@ -472,7 +523,7 @@ let onNegatedEquality tac gls =
 
 let discrSimpleClause = function
   | None -> onNegatedEquality discrEq
-  | Some (id,_,_) -> onEquality discrEq id
+  | Some ((_,id),_) -> onEquality discrEq id
 
 let discr = onEquality discrEq
 
@@ -496,8 +547,7 @@ let discrHyp id gls = discrClause (onHyp id) gls
 
 let find_sigma_data s =
   match s with  
-    | Prop Pos  -> build_sigma_set ()                    (* Set *) 
-    | Type _    -> build_sigma_type ()                   (* Type *)
+    | Prop Pos  | Type _    -> build_sigma_type ()          (* Set/Type *)
     | Prop Null -> error "find_sigma_data"
 
 (* [make_tuple env sigma (rterm,rty) lind] assumes [lind] is the lesser
@@ -505,7 +555,7 @@ let find_sigma_data s =
 
    Then we build the term
 
-     [(existS A P (mkRel lind) rterm)] of type [(sigS A P)]
+     [(existT A P (mkRel lind) rterm)] of type [(sigS A P)]
 
    where [A] is the type of [mkRel lind] and [P] is [\na:A.rty{1/lind}]
  *)
@@ -636,7 +686,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
    [make_iterated_tuple sigma env (term,typ) (z,zty)] is to build the
    tuple
 
-   [existS [xn]Pn Rel(in) .. (existS [x2]P2 Rel(i2) (existS [x1]P1 Rel(i1) z))]
+   [existT [xn]Pn Rel(in) .. (existT [x2]P2 Rel(i2) (existT [x1]P1 Rel(i1) z))]
 
    where P1 is zty[i1/x1], P2 is {x1 | P1[i2/x2]} etc.
 
@@ -651,7 +701,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
    need also to construct a default value for the other branches of
    the destructor. As default value, we take a tuple of the form
 
-    [existS [xn]Pn ?n (... existS [x2]P2 ?2 (existS [x1]P1 ?1 term))]
+    [existT [xn]Pn ?n (... existT [x2]P2 ?2 (existT [x1]P1 ?1 term))]
 
    but for this we have to solve the following unification problem:
 
@@ -866,7 +916,7 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
 
    Given that dep_pair looks like:
 
-   (existS e1 (existS e2 ... (existS en en+1) ... ))
+   (existT e1 (existT e2 ... (existT en en+1) ... ))
 
    and B might contain instances of the ei, we will return the term:
 
@@ -1010,7 +1060,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
@@ -1089,6 +1139,8 @@ let subst_all gl =
   let test (_,c) =
     try
       let (_,x,y) = snd (find_eq_data_decompose c) in
+      (* J.F.: added to prevent failure on goal containing x=x as an hyp *)
+      if eq_constr x y then failwith "caught";
       match kind_of_term x with Var x -> x | _ -> 
       match kind_of_term y with Var y -> y | _ -> failwith "caught"
     with PatternMatchingFailure -> failwith "caught"
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 3e4bfed7..9ee565c5 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: equality.mli 8651 2006-03-21 21:54:43Z jforest $ i*)
+(*i $Id: equality.mli 8780 2006-05-02 21:58:58Z letouzey $ i*)
 
 (*i*)
 open Names
@@ -43,6 +43,9 @@ val general_rewrite_bindings_in :
 val general_rewrite_in          :
   bool -> identifier -> constr -> tactic
 
+val general_multi_rewrite : 
+  bool -> constr with_bindings -> clause -> tactic
+
 val conditional_rewrite : bool -> tactic -> constr with_bindings -> tactic
 val conditional_rewrite_in :
   bool -> identifier -> tactic -> constr with_bindings -> tactic
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 73f88206..31c060f1 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evar_tactics.ml 7875 2006-01-16 09:55:24Z herbelin $ *)
+(* $Id: evar_tactics.ml 8759 2006-04-28 12:24:14Z herbelin $ *)
 
 open Term
 open Util
@@ -23,7 +23,7 @@ open Termops
 let evar_list evc c = 
   let rec evrec acc c =
     match kind_of_term c with
-    | Evar (n, _) when Evd.in_dom evc n -> c :: acc
+    | Evar (n, _) when Evd.mem evc n -> c :: acc
     | _ -> fold_constr evrec acc c
   in 
     evrec [] c
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index ca1e43cb..5a0b4b8c 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: extraargs.ml4 7841 2006-01-11 11:24:54Z herbelin $ *)
+(* $Id: extraargs.ml4 8739 2006-04-26 22:23:37Z herbelin $ *)
 
 open Pp
 open Pcoq
@@ -34,7 +34,8 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
 END
 
 (* For Setoid rewrite *)
-let pr_morphism_signature _ _ _ = Setoid_replace.pr_morphism_signature
+let pr_morphism_signature _ _ _ s =
+  spc () ++ Setoid_replace.pr_morphism_signature s
 
 ARGUMENT EXTEND morphism_signature
  TYPED AS morphism_signature
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a9ee65d7..48bd87ee 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: extratactics.ml4 8651 2006-03-21 21:54:43Z jforest $ *)
+(* $Id: extratactics.ml4 8926 2006-06-08 20:23:17Z herbelin $ *)
 
 open Pp
 open Pcoq
@@ -20,6 +20,9 @@ open Names
 (* Equality *)
 open Equality
 
+(* Pierre L: for an easy implementation of "rewrite ... in <clause>", rewrite
+  has moved to g_tactics.ml4
+
 TACTIC EXTEND rewrite
 | [ "rewrite" orient(b) constr_with_bindings(c) ] ->
     [general_rewrite_bindings b c]
@@ -30,57 +33,45 @@ TACTIC EXTEND rewrite_in
     [general_rewrite_bindings_in b h c]
 END
 
-let h_rewriteLR x = h_rewrite true (x,Rawterm.NoBindings)
+let h_rewriteLR x = h_rewrite true (x,Rawterm.NoBindings) 
+*)
 
 (* Julien: Mise en commun des differentes version de replace with in by 
-   TODO: améliorer l'affichage et deplacer dans extraargs
+   TODO: deplacer dans extraargs
 
 *)
 
-
-let pr_by_arg_tac prc _ _ opt_c = 
+let pr_by_arg_tac _prc _prlc prtac opt_c = 
   match opt_c with 
     | None -> mt ()
-    | Some c -> spc () ++ hov 2 (str "by" ++ spc ()  )
+    | Some t -> spc () ++ hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t)
 
 (* Julien Forest: on voudrait pouvoir passer la loc mais je 
 n'ai pas reussi 
 *)
 
-let pr_in_arg_hyp  = 
-fun prc _ _ opt_c->
+let pr_in_arg_hyp _prc _prlc _prtac opt_c =
   match opt_c with 
     | None -> mt ()
-    | Some c -> 
-	spc () ++ hov 2 (str "by" ++ spc () ++ 
-			   Pptactic.pr_or_var (fun _ -> mt ()) 
-			   (ArgVar(Util.dummy_loc,c))
-			)
-
-
-
+    | Some id -> spc () ++ hov 2 (str "by" ++ spc () ++ Nameops.pr_id id)
 
 ARGUMENT EXTEND by_arg_tac
   TYPED AS tactic_opt
   PRINTED BY pr_by_arg_tac
-| [ "by" tactic(c) ] -> [ Some c ]
+| [ "by" tactic3(c) ] -> [ Some c ]
 | [ ] -> [ None ]
 END
  
 ARGUMENT EXTEND in_arg_hyp
   TYPED AS ident_opt
   PRINTED BY pr_in_arg_hyp
-| [ "in" int_or_var(c) ] -> 
-    [ match c with
-	| ArgVar(_,c) ->  Some (c)
-	| _ -> Util.error "in must be used with an identifier" 
-    ]
+| [ "in" ident(c) ] -> [ Some (c) ]
 | [ ] -> [ None ]
 END
 
 TACTIC EXTEND replace 
-| ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp)  by_arg_tac(tac)  ] ->
-    [ new_replace c1 c2 in_hyp (Util.option_app Tacinterp.eval_tactic tac)  ]
+   ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ]
+-> [ new_replace c1 c2 in_hyp (Util.option_map Tacinterp.eval_tactic tac) ]
 END
 
 (* Julien:
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index d0034ca5..e42a40e7 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extratactics.mli 8651 2006-03-21 21:54:43Z jforest $ i*)
+(*i $Id: extratactics.mli 8780 2006-05-02 21:58:58Z letouzey $ i*)
 
 open Names
 open Term
@@ -15,7 +15,6 @@ open Rawterm
 
 val h_discrHyp : quantified_hypothesis -> tactic
 val h_injHyp : quantified_hypothesis -> tactic
-val h_rewriteLR : constr -> tactic
 
 val refine_tac : Genarg.open_constr -> tactic
 
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 1fe1c51e..76014955 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: hiddentac.ml 7875 2006-01-16 09:55:24Z herbelin $ *)
+(* $Id: hiddentac.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
 
 open Term
 open Proof_type
@@ -23,7 +23,7 @@ let inj_id id = (dummy_loc,id)
 
 (* Basic tactics *)
 let h_intro_move x y =
-  abstract_tactic (TacIntroMove (x, option_app inj_id y)) (intro_move x y)
+  abstract_tactic (TacIntroMove (x, option_map inj_id y)) (intro_move x y)
 let h_intro x        = h_intro_move (Some x) None
 let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x)
 let h_assumption     = abstract_tactic TacAssumption assumption
@@ -88,7 +88,9 @@ let h_simplest_right  = h_right NoBindings
 
 (* Conversion *)
 let h_reduce r cl  = abstract_tactic (TacReduce (r,cl)) (reduce r cl)
-let h_change oc c cl  = abstract_tactic (TacChange (oc,c,cl)) (change oc c cl)
+let h_change oc c cl =
+  abstract_tactic (TacChange (oc,c,cl))
+    (change (option_map Redexpr.out_with_occurrences oc) c cl)
 
 (* Equivalence relations *)
 let h_reflexivity    = abstract_tactic TacReflexivity intros_reflexivity
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index bfab1f45..df1dfde0 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: hiddentac.mli 8651 2006-03-21 21:54:43Z jforest $ i*)
+(*i $Id: hiddentac.mli 8878 2006-05-30 16:44:25Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -89,7 +89,7 @@ val h_simplest_right  : tactic
 (* Conversion *)
 val h_reduce          : Redexpr.red_expr -> Tacticals.clause -> tactic
 val h_change          :
-  constr occurrences option -> constr -> Tacticals.clause -> tactic
+  constr with_occurrences option -> constr -> Tacticals.clause -> tactic
 
 (* Equivalence relations *)
 val h_reflexivity     : tactic
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 64a0e0f1..fca84fd2 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*)
 
-(* $Id: hipattern.ml4 8652 2006-03-22 08:27:14Z herbelin $ *)
+(* $Id: hipattern.ml4 8866 2006-05-28 16:21:04Z herbelin $ *)
 
 open Pp
 open Util
@@ -279,7 +279,6 @@ let dest_nf_eq gls eqn =
 
 (* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *)
 let coq_ex_pattern_gen ex = lazy PATTERN [ %ex ?X1 ?X2 ?X3 ?X4 ]
-let coq_existS_pattern = coq_ex_pattern_gen coq_existS_ref
 let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref
 
 let match_sigma ex ex_pat =
@@ -292,8 +291,7 @@ let match_sigma ex ex_pat =
 
 let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *)
   first_match (match_sigma ex) 
-    [coq_existS_pattern, build_sigma_set; 
-     coq_existT_pattern, build_sigma_type]
+    [coq_existT_pattern, build_sigma_type]
 
 (* Pattern "(sig ?1 ?2)" *)
 let coq_sig_pattern = lazy PATTERN [ %coq_sig_ref ?X1 ?X2 ]
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 1627a8ca..86cd191e 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: hipattern.mli 8652 2006-03-22 08:27:14Z herbelin $ i*)
+(*i $Id: hipattern.mli 8866 2006-05-28 16:21:04Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -101,7 +101,7 @@ open Coqlib
 val find_eq_data_decompose : constr -> 
   coq_leibniz_eq_data * (constr * constr * constr)
 
-(* Match a term of the form [(existS A P t p)] or [(existT A P t p)] *)
+(* Match a term of the form [(existT A P t p)] *)
 (* Returns associated lemmas and [A,P,t,p] *)
 val find_sigma_data_decompose : constr -> 
   coq_sigma_data * (constr * constr * constr * constr)
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index 0867d220..554ce2e9 100644
--- a/tactics/nbtermdn.ml
+++ b/tactics/nbtermdn.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: nbtermdn.ml 6427 2004-12-07 17:41:10Z sacerdot $ *)
+(* $Id: nbtermdn.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
 
 open Util
 open Names
@@ -43,14 +43,14 @@ let get_dn dnm hkey =
   try Gmap.find hkey dnm with Not_found -> Btermdn.create ()
 
 let add dn (na,(pat,valu)) =
-  let hkey = option_app fst (Termdn.constr_pat_discr pat) in 
+  let hkey = option_map fst (Termdn.constr_pat_discr pat) in 
   dn.table <- Gmap.add na (pat,valu) dn.table;
   let dnm = dn.patterns in
   dn.patterns <- Gmap.add hkey (Btermdn.add (get_dn dnm hkey) (pat,valu)) dnm
     
 let rmv dn na =
   let (pat,valu) = Gmap.find na dn.table in
-  let hkey = option_app fst (Termdn.constr_pat_discr pat) in 
+  let hkey = option_map fst (Termdn.constr_pat_discr pat) in 
   dn.table <- Gmap.remove na dn.table;
   let dnm = dn.patterns in
   dn.patterns <- Gmap.add hkey (Btermdn.rmv (get_dn dnm hkey) (pat,valu)) dnm
@@ -62,7 +62,7 @@ let remap ndn na (pat,valu) =
   add ndn (na,(pat,valu))
 
 let lookup dn valu =
-  let hkey = option_app fst (Termdn.constr_val_discr valu) in 
+  let hkey = option_map fst (Termdn.constr_val_discr valu) in 
   try Btermdn.lookup (Gmap.find hkey  dn.patterns) valu with Not_found -> []
 
 let app f dn = Gmap.iter f dn.table
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index a6331927..8c8d4d37 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: setoid_replace.ml 8683 2006-04-05 15:47:39Z letouzey $ *)
+(* $Id: setoid_replace.ml 8900 2006-06-06 14:40:27Z letouzey $ *)
 
 open Tacmach
 open Proof_type
@@ -85,7 +85,7 @@ type morphism_class =
 let subst_mps_in_relation_class subst =
  function
     Relation  t -> Relation  (subst_mps subst t)
-  | Leibniz t -> Leibniz (option_app (subst_mps subst) t) 
+  | Leibniz t -> Leibniz (option_map (subst_mps subst) t) 
 
 let subst_mps_in_argument_class subst (variance,rel) =
  variance, subst_mps_in_relation_class subst rel
@@ -295,9 +295,9 @@ let relation_morphism_of_constr_morphism =
 let subst_relation subst relation = 
   let rel_a' = subst_mps subst relation.rel_a in
   let rel_aeq' = subst_mps subst relation.rel_aeq in
-  let rel_refl' = option_app (subst_mps subst) relation.rel_refl in
-  let rel_sym' = option_app (subst_mps subst) relation.rel_sym in
-  let rel_trans' = option_app (subst_mps subst) relation.rel_trans in
+  let rel_refl' = option_map (subst_mps subst) relation.rel_refl in
+  let rel_sym' = option_map (subst_mps subst) relation.rel_sym in
+  let rel_trans' = option_map (subst_mps subst) relation.rel_trans in
   let rel_X_relation_class' = subst_mps subst relation.rel_X_relation_class in
   let rel_Xreflexive_relation_class' =
    subst_mps subst relation.rel_Xreflexive_relation_class
@@ -638,9 +638,9 @@ let apply_to_relation subst rel =
    assert (new_quantifiers_no >= 0) ;
    { rel_a = mkApp (rel.rel_a, subst) ;
      rel_aeq = mkApp (rel.rel_aeq, subst) ;
-     rel_refl = option_app (fun c -> mkApp (c,subst)) rel.rel_refl ; 
-     rel_sym = option_app (fun c -> mkApp (c,subst)) rel.rel_sym;
-     rel_trans = option_app (fun c -> mkApp (c,subst)) rel.rel_trans;
+     rel_refl = option_map (fun c -> mkApp (c,subst)) rel.rel_refl ; 
+     rel_sym = option_map (fun c -> mkApp (c,subst)) rel.rel_sym;
+     rel_trans = option_map (fun c -> mkApp (c,subst)) rel.rel_trans;
      rel_quantifiers_no = new_quantifiers_no;
      rel_X_relation_class = mkApp (rel.rel_X_relation_class, subst);
      rel_Xreflexive_relation_class =
@@ -763,6 +763,8 @@ let unify_relation_class_carrier_with_type env rel t =
   | Leibniz None -> Leibniz (Some t)
   | Relation rel -> Relation (unify_relation_carrier_with_type env rel t)
 
+exception Impossible
+
 (* first order matching with a bit of conversion *)
 (* Note: the type checking operations performed by the function could  *)
 (* be done once and for all abstracting the morphism structure using   *)
@@ -772,27 +774,28 @@ let unify_relation_class_carrier_with_type env rel t =
 let unify_morphism_with_arguments gl (c,av)
      {args=args; output=output; lem=lem; morphism_theory=morphism_theory} t
 =
- let al = Array.to_list av in
+ let avlen = Array.length av in 
  let argsno = List.length args in
- let quantifiers,al' = Util.list_chop (List.length al - argsno) al in
+ if avlen < argsno then raise Impossible; (* partial application *)
+ let al = Array.to_list av in
+ let quantifiers,al' = Util.list_chop (avlen - argsno) al in
  let quantifiersv = Array.of_list quantifiers in
  let c' = mkApp (c,quantifiersv) in
- if dependent t c' then None else (
-  (* these are pf_type_of we could avoid *)
-  let al'_type = List.map (Tacmach.pf_type_of gl) al' in
-  let args' =
+ if dependent t c' then raise Impossible; 
+ (* these are pf_type_of we could avoid *)
+ let al'_type = List.map (Tacmach.pf_type_of gl) al' in
+ let args' =
    List.map2
-    (fun (var,rel) ty ->
-      var,unify_relation_class_carrier_with_type (pf_env gl) rel ty)
-    args al'_type in
-  (* this is another pf_type_of we could avoid *)
-  let ty = Tacmach.pf_type_of gl (mkApp (c,av)) in
-  let output' = unify_relation_class_carrier_with_type (pf_env gl) output ty in
-  let lem' = mkApp (lem,quantifiersv) in
-  let morphism_theory' = mkApp (morphism_theory,quantifiersv) in
-   Some
-    ({args=args'; output=output'; lem=lem'; morphism_theory=morphism_theory'},
-     c',Array.of_list al'))
+     (fun (var,rel) ty ->
+	var,unify_relation_class_carrier_with_type (pf_env gl) rel ty)
+     args al'_type in
+ (* this is another pf_type_of we could avoid *)
+ let ty = Tacmach.pf_type_of gl (mkApp (c,av)) in
+ let output' = unify_relation_class_carrier_with_type (pf_env gl) output ty in
+ let lem' = mkApp (lem,quantifiersv) in
+ let morphism_theory' = mkApp (morphism_theory,quantifiersv) in
+ ({args=args'; output=output'; lem=lem'; morphism_theory=morphism_theory'},
+  c',Array.of_list al')
 
 let new_morphism m signature id hook =
  if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
@@ -1078,9 +1081,9 @@ let int_add_relation id a aeq refl sym trans =
       let a_instance = apply_to_rels a a_quantifiers_rev in
       let aeq_instance = apply_to_rels aeq a_quantifiers_rev in
       let sym_instance =
-       option_app (fun x -> apply_to_rels x a_quantifiers_rev) sym in
+       option_map (fun x -> apply_to_rels x a_quantifiers_rev) sym in
       let refl_instance =
-       option_app (fun x -> apply_to_rels x a_quantifiers_rev) refl in
+       option_map (fun x -> apply_to_rels x a_quantifiers_rev) refl in
       let trans_instance = apply_to_rels trans a_quantifiers_rev in
       let aeq_rel_class_and_var1, aeq_rel_class_and_var2, lemma, output =
        match sym_instance, refl_instance with
@@ -1134,8 +1137,8 @@ let int_add_relation id a aeq refl sym trans =
 
 (* The vernac command "Add Relation ..." *)
 let add_relation id a aeq refl sym trans =
- int_add_relation id (constr_of a) (constr_of aeq) (option_app constr_of refl)
-  (option_app constr_of sym) (option_app constr_of trans)
+ int_add_relation id (constr_of a) (constr_of aeq) (option_map constr_of refl)
+  (option_map constr_of sym) (option_map constr_of trans)
 
 (************************ Add Setoid ******************************************)
 
@@ -1383,10 +1386,9 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction =
           let mors_and_cs_and_als =
            List.fold_left
             (fun l (m,c,al) ->
-              match unify_morphism_with_arguments gl (c,al) m t with
-                 Some res -> res::l
-               | None -> l
-            ) [] mors_and_cs_and_als
+	       try (unify_morphism_with_arguments gl (c,al) m t) :: l
+	       with Impossible -> l
+	    ) [] mors_and_cs_and_als
           in
            List.filter
             (fun (mor,_,_) -> subrelation gl mor.output output_relation)
@@ -1817,12 +1819,20 @@ let relation_rewrite_in id c1 c2 (direction,eqclause) ~new_goals gl =
  (* since we will actually rewrite in the opposite direction, we also need
     to replace every occurrence of c2 (resp. c1) in hyp with something that
     is convertible but not syntactically equal. To this aim we introduce a
-    let-in and then we will use the intro tactic to get rid of it *)
- let let_in_abstract t in_t =
-  let t' = lift 1 t in
-  let in_t' = lift 1 in_t in
-   mkLetIn (Anonymous,t,pf_type_of gl t,subst_term t' in_t') in
- let mangled_new_hyp = Termops.replace_term c1 c2 (let_in_abstract c2 hyp) in
+    let-in and then we will use the intro tactic to get rid of it.
+    Quite tricky to do properly since c1 can occur in c2 or vice-versa ! *)
+ let mangled_new_hyp = 
+   let hyp = lift 2 hyp in 
+   (* first, we backup every occurences of c1 in newly allocated (Rel 1) *)
+   let hyp = Termops.replace_term (lift 2 c1) (mkRel 1) hyp in 
+   (* then, we factorize every occurences of c2 into (Rel 2) *)
+   let hyp = Termops.replace_term (lift 2 c2) (mkRel 2) hyp in 
+   (* Now we substitute (Rel 1) (i.e. c1) for c2 *)
+   let hyp = subst1 (lift 1 c2) hyp in 
+   (* Since subst1 has killed Rel 1 and decreased the other Rels, 
+      Rel 1 is now coding for c2, we can build the let-in factorizing c2 *)
+   mkLetIn (Anonymous,c2,pf_type_of gl c2,hyp) 
+ in 
  let new_hyp = Termops.replace_term c1 c2 hyp in 
  let oppdir = opposite_direction direction in 
  cut_replacing id new_hyp
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index 5dc691a9..750addcc 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: setoid_replace.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
+(*i $Id: setoid_replace.mli 8779 2006-05-02 20:59:21Z letouzey $ i*)
 
 open Term
 open Proof_type
@@ -75,3 +75,6 @@ val add_setoid :
 
 val new_named_morphism :
  Names.identifier -> constr_expr -> morphism_signature option -> unit
+
+val relation_table_find : constr -> relation
+val relation_table_mem : constr -> bool
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e2487c4e..0f487009 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacinterp.ml 8654 2006-03-22 15:36:58Z msozeau $ *)
+(* $Id: tacinterp.ml 8926 2006-06-08 20:23:17Z herbelin $ *)
 
 open Constrintern
 open Closure
@@ -46,6 +46,7 @@ open Inductiveops
 open Syntax_def
 open Pretyping
 open Pretyping.Default
+open Pcoq
 
 let error_syntactic_metavariables_not_allowed loc =
   user_err_loc 
@@ -514,7 +515,7 @@ let intern_redexp ist = function
   | Cbv f -> Cbv (intern_flag ist f)
   | Lazy f -> Lazy (intern_flag ist f)
   | Pattern l -> Pattern (List.map (intern_constr_occurrence ist) l)
-  | Simpl o -> Simpl (option_app (intern_constr_occurrence ist) o)
+  | Simpl o -> Simpl (option_map (intern_constr_occurrence ist) o)
   | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r
   
 
@@ -523,14 +524,14 @@ let intern_inversion_strength lf ist = function
       NonDepInversion (k,List.map (intern_hyp_or_metaid ist) idl,
       intern_intro_pattern lf ist ids)
   | DepInversion (k,copt,ids) ->
-      DepInversion (k, option_app (intern_constr ist) copt,
+      DepInversion (k, option_map (intern_constr ist) copt,
       intern_intro_pattern lf ist ids)
   | InversionUsing (c,idl) ->
       InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl)
 
 (* Interprets an hypothesis name *)
-let intern_hyp_location ist (id,occs,hl) =
-  (intern_hyp ist (skip_metaid id), occs, hl)
+let intern_hyp_location ist ((occs,id),hl) =
+  ((List.map (intern_int_or_var ist) occs,intern_hyp ist (skip_metaid id)), hl)
 
 let interp_constrpattern_gen sigma env ltacvar c =
   let c = intern_gen false ~allow_soapp:true ~ltacvars:(ltacvar,[])
@@ -618,29 +619,29 @@ let rec intern_atomic lf ist x =
       TacIntroPattern (List.map (intern_intro_pattern lf ist) l)
   | TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp)
   | TacIntroMove (ido,ido') ->
-      TacIntroMove (option_app (intern_ident lf ist) ido,
-          option_app (intern_hyp ist) ido')
+      TacIntroMove (option_map (intern_ident lf ist) ido,
+          option_map (intern_hyp ist) ido')
   | TacAssumption -> TacAssumption
   | TacExact c -> TacExact (intern_constr ist c)
   | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
   | TacApply cb -> TacApply (intern_constr_with_bindings ist cb)
   | TacElim (cb,cbo) ->
       TacElim (intern_constr_with_bindings ist cb,
-               option_app (intern_constr_with_bindings ist) cbo)
+               option_map (intern_constr_with_bindings ist) cbo)
   | TacElimType c -> TacElimType (intern_type ist c)
   | TacCase cb -> TacCase (intern_constr_with_bindings ist cb)
   | TacCaseType c -> TacCaseType (intern_type ist c)
-  | TacFix (idopt,n) -> TacFix (option_app (intern_ident lf ist) idopt,n)
+  | TacFix (idopt,n) -> TacFix (option_map (intern_ident lf ist) idopt,n)
   | TacMutualFix (id,n,l) ->
       let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
       TacMutualFix (intern_ident lf ist id, n, List.map f l)
-  | TacCofix idopt -> TacCofix (option_app (intern_ident lf ist) idopt)
+  | TacCofix idopt -> TacCofix (option_map (intern_ident lf ist) idopt)
   | TacMutualCofix (id,l) ->
       let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
       TacMutualCofix (intern_ident lf ist id, List.map f l)
   | TacCut c -> TacCut (intern_type ist c)
   | TacAssert (otac,ipat,c) ->
-      TacAssert (option_app (intern_tactic ist) otac,
+      TacAssert (option_map (intern_tactic ist) otac,
                  intern_intro_pattern lf ist ipat,
                  intern_constr_gen (otac<>None) ist c)
   | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl)
@@ -660,26 +661,26 @@ let rec intern_atomic lf ist x =
   (* Automation tactics *)
   | TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l)
   | TacAuto (n,lems,l) ->
-      TacAuto (option_app (intern_int_or_var ist) n,
+      TacAuto (option_map (intern_int_or_var ist) n,
         List.map (intern_constr ist) lems,l)
   | TacAutoTDB n -> TacAutoTDB n
   | TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id)
   | TacDestructConcl -> TacDestructConcl
   | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
-  | TacDAuto (n,p) -> TacDAuto (option_app (intern_int_or_var ist) n,p)
+  | TacDAuto (n,p) -> TacDAuto (option_map (intern_int_or_var ist) n,p)
 
   (* Derived basic tactics *)
   | TacSimpleInduction h ->
       TacSimpleInduction (intern_quantified_hypothesis ist h)
   | TacNewInduction (lc,cbo,ids) ->
       TacNewInduction (List.map (intern_induction_arg ist) lc,
-               option_app (intern_constr_with_bindings ist) cbo,
+               option_map (intern_constr_with_bindings ist) cbo,
                (intern_intro_pattern lf ist ids))
   | TacSimpleDestruct h ->
       TacSimpleDestruct (intern_quantified_hypothesis ist h)
   | TacNewDestruct (c,cbo,ids) ->
       TacNewDestruct (List.map (intern_induction_arg ist) c,
-               option_app (intern_constr_with_bindings ist) cbo,
+               option_map (intern_constr_with_bindings ist) cbo,
 	       (intern_intro_pattern lf ist ids))
   | TacDoubleInduction (h1,h2) ->
       let h1 = intern_quantified_hypothesis ist h1 in
@@ -703,14 +704,14 @@ let rec intern_atomic lf ist x =
   | TacLeft bl -> TacLeft (intern_bindings ist bl)
   | TacRight bl -> TacRight (intern_bindings ist bl)
   | TacSplit (b,bl) -> TacSplit (b,intern_bindings ist bl)
-  | TacAnyConstructor t -> TacAnyConstructor (option_app (intern_tactic ist) t)
+  | TacAnyConstructor t -> TacAnyConstructor (option_map (intern_tactic ist) t)
   | TacConstructor (n,bl) -> TacConstructor (n, intern_bindings ist bl)
 
   (* Conversion *)
   | TacReduce (r,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,
+      TacChange (option_map (intern_constr_occurrence ist) occl,
         intern_constr ist c, clause_app (intern_hyp_location ist) cl)
 
   (* Equivalence relations *)
@@ -720,6 +721,9 @@ let rec intern_atomic lf ist x =
   | TacTransitivity c -> TacTransitivity (intern_constr ist c)
 
   (* Equality and inversion *)
+  | TacRewrite (b,c,cl) -> 
+      TacRewrite (b,intern_constr_with_bindings ist c,
+		  clause_app (intern_hyp_location ist) cl)
   | TacInversion (inv,hyp) ->
       TacInversion (intern_inversion_strength lf ist inv,
         intern_quantified_hypothesis ist hyp)
@@ -750,7 +754,7 @@ and intern_tactic_seq ist = function
   | TacLetIn (l,u) ->
       let l = List.map
         (fun (n,c,b) ->
-          (n,option_app (intern_tactic ist) c, intern_tacarg !strict_check ist b)) l in
+          (n,option_map (intern_tactic ist) c, intern_tacarg !strict_check ist b)) l in
       let (l1,l2) = ist.ltacvars in
       let ist' = { ist with ltacvars = ((extract_let_names l)@l1,l2) } in
       ist.ltacvars, TacLetIn (l,intern_tactic ist' u)
@@ -864,9 +868,6 @@ and intern_genarg ist x =
         (intern_quantified_hypothesis ist (out_gen rawwit_quant_hyp x))
   | RedExprArgType ->
       in_gen globwit_red_expr (intern_redexp ist (out_gen rawwit_red_expr x))
-  | TacticArgType n ->
-      in_gen (globwit_tactic n) (intern_tactic ist
-	(out_gen (rawwit_tactic n) x))
   | OpenConstrArgType b ->
       in_gen (globwit_open_constr_gen b)
         ((),intern_constr ist (snd (out_gen (rawwit_open_constr_gen b) x)))
@@ -880,7 +881,14 @@ and intern_genarg ist x =
   | List1ArgType _ -> app_list1 (intern_genarg ist) x
   | OptArgType _ -> app_opt (intern_genarg ist) x
   | PairArgType _ -> app_pair (intern_genarg ist) (intern_genarg ist) x
-  | ExtraArgType s -> lookup_genarg_glob s ist x
+  | ExtraArgType s ->
+      match tactic_genarg_level s with
+      | Some n -> 
+          (* Special treatment of tactic arguments *)
+          in_gen (globwit_tactic n) (intern_tactic ist
+	    (out_gen (rawwit_tactic n) x))
+      | None ->
+          lookup_genarg_glob s ist x
 
 (************* End globalization ************)
 
@@ -1121,10 +1129,12 @@ let interp_evaluable ist env = function
   | ArgVar (_,id) -> coerce_to_evaluable_ref env (List.assoc id ist.lfun)
 
 (* Interprets an hypothesis name *)
-let interp_hyp_location ist gl (id,occs,hl) = (interp_hyp ist gl id,occs,hl)
+let interp_hyp_location ist gl ((occs,id),hl) =
+  ((List.map (fun n -> ArgArg (interp_int_or_var ist n)) occs,
+    interp_hyp ist gl id),hl)
 
 let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } =
-  { onhyps=option_app(List.map (interp_hyp_location ist gl)) ol;
+  { onhyps=option_map(List.map (interp_hyp_location ist gl)) ol;
     onconcl=b;
     concl_occs=occs }
 
@@ -1194,11 +1204,11 @@ let solve_remaining_evars env initial_sigma evars c =
   let isevars = ref evars in
   let rec proc_rec c =
     match kind_of_term (Reductionops.whd_evar (evars_of !isevars) c) with
-      | Evar (ev,args as k) when not (Evd.in_dom initial_sigma ev) ->
+      | Evar (ev,args as k) when not (Evd.mem initial_sigma ev) ->
             let (loc,src) = evar_source ev !isevars in
 	    let sigma = evars_of !isevars in
 	    (try 
-	      let evi = Evd.map sigma ev in
+	      let evi = Evd.find sigma ev in
 	      let c = solvable_by_tactic env evi k src in
 	      isevars := Evd.evar_define ev c !isevars;
 	      c
@@ -1261,7 +1271,9 @@ let interp_unfold ist env (l,qid) =
 let interp_flag ist env red =
   { red with rConst = List.map (interp_evaluable ist env) red.rConst }
 
-let interp_pattern ist sigma env (l,c) = (l,interp_constr ist sigma env c)
+let interp_pattern ist sigma env (l,c) = 
+  (List.map (fun n -> ArgArg (interp_int_or_var ist n)) l,
+   interp_constr ist sigma env c)
 
 let pf_interp_pattern ist gl = interp_pattern ist (project gl) (pf_env gl)
 
@@ -1271,7 +1283,7 @@ let redexp_interp ist sigma env = function
   | Cbv f -> Cbv (interp_flag ist env f)
   | Lazy f -> Lazy (interp_flag ist env f)
   | Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l)
-  | Simpl o -> Simpl (option_app (interp_pattern ist sigma env) o)
+  | Simpl o -> Simpl (option_map (interp_pattern ist sigma env) o)
   | (Red _ |  Hnf | ExtraRedExpr _ | CbvVm as r) -> r
 
 let pf_redexp_interp ist gl = redexp_interp ist (project gl) (pf_env gl)
@@ -1568,7 +1580,7 @@ and interp_match_context ist g lz lr lmr =
            db_matched_concl ist.debug (pf_env goal) concl;
            apply_hyps_context ist env lz goal mt [] lgoal mhyps hyps
         with e when is_match_catchable e ->
-          (match e with
+         (match e with
             | PatternMatchingFailure -> db_matching_failure ist.debug
             | Eval_fail s -> db_eval_failure ist.debug s
             | _ -> db_logic_failure ist.debug e);
@@ -1652,7 +1664,6 @@ and interp_genarg ist goal x =
           (out_gen globwit_quant_hyp x))
   | RedExprArgType ->
       in_gen wit_red_expr (pf_redexp_interp ist goal (out_gen globwit_red_expr x))
-  | TacticArgType n -> in_gen (wit_tactic n) (out_gen (globwit_tactic n) x)
   | OpenConstrArgType casted ->
       in_gen (wit_open_constr_gen casted) 
         (pf_interp_open_constr casted ist goal 
@@ -1667,7 +1678,13 @@ and interp_genarg ist goal x =
   | List1ArgType _ -> app_list1 (interp_genarg ist goal) x
   | OptArgType _ -> app_opt (interp_genarg ist goal) x
   | PairArgType _ -> app_pair (interp_genarg ist goal) (interp_genarg ist goal) x
-  | ExtraArgType s -> lookup_interp_genarg s ist goal x
+  | ExtraArgType s -> 
+      match tactic_genarg_level s with
+      | Some n -> 
+          (* Special treatment of tactic arguments *)
+          in_gen (wit_tactic n) (out_gen (globwit_tactic n) x)
+      | None -> 
+          lookup_interp_genarg s ist goal x
 
 (* Interprets the Match expressions *)
 and interp_match ist g lz constr lmr =
@@ -1719,23 +1736,23 @@ and interp_atomic ist gl = function
   | TacIntrosUntil hyp ->
       h_intros_until (interp_quantified_hypothesis ist hyp)
   | TacIntroMove (ido,ido') ->
-      h_intro_move (option_app (interp_ident ist) ido)
-      (option_app (interp_hyp ist gl) ido')
+      h_intro_move (option_map (interp_ident ist) ido)
+      (option_map (interp_hyp ist gl) ido')
   | TacAssumption -> h_assumption
   | TacExact c -> h_exact (pf_interp_casted_constr ist gl c)
   | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c)
   | TacApply cb -> h_apply (interp_constr_with_bindings ist gl cb)
   | TacElim (cb,cbo) ->
       h_elim (interp_constr_with_bindings ist gl cb)
-                (option_app (interp_constr_with_bindings ist gl) cbo)
+                (option_map (interp_constr_with_bindings ist gl) cbo)
   | TacElimType c -> h_elim_type (pf_interp_type ist gl c)
   | TacCase cb -> h_case (interp_constr_with_bindings ist gl cb)
   | TacCaseType c -> h_case_type (pf_interp_type ist gl c)
-  | TacFix (idopt,n) -> h_fix (option_app (interp_ident ist) idopt) n
+  | TacFix (idopt,n) -> h_fix (option_map (interp_ident ist) idopt) n
   | TacMutualFix (id,n,l) ->
       let f (id,n,c) = (interp_ident ist id,n,pf_interp_type ist gl c) in
       h_mutual_fix (interp_ident ist id) n (List.map f l)
-  | TacCofix idopt -> h_cofix (option_app (interp_ident ist) idopt)
+  | TacCofix idopt -> h_cofix (option_map (interp_ident ist) idopt)
   | TacMutualCofix (id,l) ->
       let f (id,c) = (interp_ident ist id,pf_interp_type ist gl c) in
       h_mutual_cofix (interp_ident ist id) (List.map f l)
@@ -1743,7 +1760,7 @@ and interp_atomic ist gl = function
   | TacAssert (t,ipat,c) ->
       let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in
       abstract_tactic (TacAssert (t,ipat,c))
-        (Tactics.forward (option_app (interp_tactic ist) t)
+        (Tactics.forward (option_map (interp_tactic ist) t)
 	  (interp_intro_pattern ist ipat) c)
   | TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl)
   | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
@@ -1760,29 +1777,29 @@ and interp_atomic ist gl = function
   (* Automation tactics *)
   | TacTrivial (lems,l) -> 
       Auto.h_trivial (List.map (pf_interp_constr ist gl) lems)
-	(option_app (List.map (interp_hint_base ist)) l)
+	(option_map (List.map (interp_hint_base ist)) l)
   | TacAuto (n,lems,l) ->
-      Auto.h_auto (option_app (interp_int_or_var ist) n)
+      Auto.h_auto (option_map (interp_int_or_var ist) n)
       (List.map (pf_interp_constr ist gl) lems)
-      (option_app (List.map (interp_hint_base ist)) l)
+      (option_map (List.map (interp_hint_base ist)) l)
   | TacAutoTDB n -> Dhyp.h_auto_tdb n
   | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id)
   | TacDestructConcl -> Dhyp.h_destructConcl
   | TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2
-  | TacDAuto (n,p) -> Auto.h_dauto (option_app (interp_int_or_var ist) n,p)
+  | TacDAuto (n,p) -> Auto.h_dauto (option_map (interp_int_or_var ist) n,p)
 
   (* Derived basic tactics *)
   | TacSimpleInduction h ->
       h_simple_induction (interp_quantified_hypothesis ist h)
   | TacNewInduction (lc,cbo,ids) ->
       h_new_induction (List.map (interp_induction_arg ist gl) lc)
-        (option_app (interp_constr_with_bindings ist gl) cbo)
+        (option_map (interp_constr_with_bindings ist gl) cbo)
         (interp_intro_pattern ist ids)
   | TacSimpleDestruct h ->
       h_simple_destruct (interp_quantified_hypothesis ist h)
   | TacNewDestruct (c,cbo,ids) -> 
       h_new_destruct (List.map (interp_induction_arg ist gl) c)
-        (option_app (interp_constr_with_bindings ist gl) cbo)
+        (option_map (interp_constr_with_bindings ist gl) cbo)
         (interp_intro_pattern ist ids)
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist h1 in
@@ -1811,7 +1828,7 @@ and interp_atomic ist gl = function
   | TacSplit (_,bl) -> h_split (interp_bindings ist gl bl)
   | TacAnyConstructor t ->
       abstract_tactic (TacAnyConstructor t)
-        (Tactics.any_constructor (option_app (interp_tactic ist) t))
+        (Tactics.any_constructor (option_map (interp_tactic ist) t))
   | TacConstructor (n,bl) ->
       h_constructor (skip_metaid n) (interp_bindings ist gl bl)
 
@@ -1819,7 +1836,7 @@ and interp_atomic ist gl = function
   | TacReduce (r,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)
+      h_change (option_map (pf_interp_pattern ist gl) occl)
         (pf_interp_constr ist gl c) (interp_clause ist gl cl)
 
   (* Equivalence relations *)
@@ -1828,8 +1845,12 @@ and interp_atomic ist gl = function
   | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c)
 
   (* Equality and inversion *)
+  | TacRewrite (b,c,cl) -> 
+      Equality.general_multi_rewrite b 
+	(interp_constr_with_bindings ist gl c) 
+	(interp_clause ist gl cl)
   | TacInversion (DepInversion (k,c,ids),hyp) ->
-      Inv.dinv k (option_app (pf_interp_constr ist gl) c)
+      Inv.dinv k (option_map (pf_interp_constr ist gl) c)
         (interp_intro_pattern ist ids)
         (interp_declared_or_quantified_hypothesis ist gl hyp)
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
@@ -1868,13 +1889,17 @@ and interp_atomic ist gl = function
     | ConstrMayEvalArgType ->
 	VConstr
           (interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x))
-    | TacticArgType n -> 
-	val_interp ist gl (out_gen (globwit_tactic n) x)
+    | ExtraArgType s when tactic_genarg_level s <> None ->
+          (* Special treatment of tactic arguments *)
+	val_interp ist gl 
+          (out_gen (globwit_tactic (out_some (tactic_genarg_level s))) x)
     | StringArgType | BoolArgType
     | QuantHypArgType | RedExprArgType 
-    | OpenConstrArgType _ | ConstrWithBindingsArgType | BindingsArgType 
-    | ExtraArgType _ | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ 
+    | OpenConstrArgType _ | ConstrWithBindingsArgType 
+    | ExtraArgType _ | BindingsArgType 
+    | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ 
 	-> error "This generic type is not supported in alias"
+        
     in
     let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in
     let v = locate_tactic_call loc (val_interp { ist with lfun=lfun } gl body)
@@ -1938,7 +1963,7 @@ let subst_and_short_name f (c,n) =
 
 let subst_or_var f =  function
   | ArgVar _ as x -> x
-  | ArgArg (x) -> ArgArg (f x)
+  | ArgArg x -> ArgArg (f x)
 
 let subst_located f (_loc,id) = (loc,f id)
 
@@ -1977,7 +2002,7 @@ let subst_redexp subst = function
   | Cbv f -> Cbv (subst_flag subst f)
   | Lazy f -> Lazy (subst_flag subst f)
   | Pattern l -> Pattern (List.map (subst_constr_occurrence subst) l)
-  | Simpl o -> Simpl (option_app (subst_constr_occurrence subst) o)
+  | Simpl o -> Simpl (option_map (subst_constr_occurrence subst) o)
   | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r
 
 let subst_raw_may_eval subst = function
@@ -2005,7 +2030,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacApply cb -> TacApply (subst_raw_with_bindings subst cb)
   | TacElim (cb,cbo) ->
       TacElim (subst_raw_with_bindings subst cb,
-               option_app (subst_raw_with_bindings subst) cbo)
+               option_map (subst_raw_with_bindings subst) cbo)
   | TacElimType c -> TacElimType (subst_rawconstr subst c)
   | TacCase cb -> TacCase (subst_raw_with_bindings subst cb)
   | TacCaseType c -> TacCaseType (subst_rawconstr subst c)
@@ -2035,11 +2060,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacSimpleInduction h as x -> x
   | TacNewInduction (lc,cbo,ids) -> (* Pierre C. est-ce correct? *)
       TacNewInduction (List.map (subst_induction_arg subst) lc,
-               option_app (subst_raw_with_bindings subst) cbo, ids)
+               option_map (subst_raw_with_bindings subst) cbo, ids)
   | TacSimpleDestruct h as x -> x
   | TacNewDestruct (c,cbo,ids) ->
       TacNewDestruct (List.map (subst_induction_arg subst) c,  (* Julien F. est-ce correct? *)
-               option_app (subst_raw_with_bindings subst) cbo, ids)
+               option_map (subst_raw_with_bindings subst) cbo, ids)
   | TacDoubleInduction (h1,h2) as x -> x
   | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c)
   | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c)
@@ -2059,13 +2084,13 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacLeft bl -> TacLeft (subst_bindings subst bl)
   | TacRight bl -> TacRight (subst_bindings subst bl)
   | TacSplit (b,bl) -> TacSplit (b,subst_bindings subst bl)
-  | TacAnyConstructor t -> TacAnyConstructor (option_app (subst_tactic subst) t)
+  | TacAnyConstructor t -> TacAnyConstructor (option_map (subst_tactic subst) t)
   | TacConstructor (n,bl) -> TacConstructor (n, subst_bindings subst bl)
 
   (* Conversion *)
   | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl)
   | TacChange (occl,c,cl) ->
-      TacChange (option_app (subst_constr_occurrence subst) occl,
+      TacChange (option_map (subst_constr_occurrence subst) occl,
         subst_rawconstr subst c, cl)
 
   (* Equivalence relations *)
@@ -2073,8 +2098,9 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacTransitivity c -> TacTransitivity (subst_rawconstr subst c)
 
   (* Equality and inversion *)
+  | TacRewrite (b,c,cl) -> TacRewrite (b, subst_raw_with_bindings subst c,cl)
   | TacInversion (DepInversion (k,c,l),hyp) ->
-     TacInversion (DepInversion (k,option_app (subst_rawconstr subst) c,l),hyp)
+     TacInversion (DepInversion (k,option_map (subst_rawconstr subst) c,l),hyp)
   | TacInversion (NonDepInversion _,_) as x -> x
   | TacInversion (InversionUsing (c,cl),hyp) ->
       TacInversion (InversionUsing (subst_rawconstr subst c,cl),hyp)
@@ -2093,7 +2119,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
       let lrc = List.map (fun (n,b) -> (n,subst_tactic_fun subst b)) lrc in
       TacLetRecIn (lrc,(subst_tactic subst u:glob_tactic_expr))
   | TacLetIn (l,u) ->
-      let l = List.map (fun (n,c,b) -> (n,option_app (subst_tactic subst) c,subst_tacarg subst b)) l in
+      let l = List.map (fun (n,c,b) -> (n,option_map (subst_tactic subst) c,subst_tacarg subst b)) l in
       TacLetIn (l,subst_tactic subst u)
   | TacMatchContext (lz,lr,lmr) ->
       TacMatchContext(lz,lr, subst_match_rule subst lmr)
@@ -2172,9 +2198,6 @@ and subst_genarg subst (x:glob_generic_argument) =
           (out_gen globwit_quant_hyp x))
   | RedExprArgType ->
       in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x))
-  | TacticArgType n ->
-      in_gen (globwit_tactic n)
-        (subst_tactic subst (out_gen (globwit_tactic n) x))
   | OpenConstrArgType b ->
       in_gen (globwit_open_constr_gen b)
         ((),subst_rawconstr subst (snd (out_gen (globwit_open_constr_gen b) x)))
@@ -2188,7 +2211,14 @@ and subst_genarg subst (x:glob_generic_argument) =
   | List1ArgType _ -> app_list1 (subst_genarg subst) x
   | OptArgType _ -> app_opt (subst_genarg subst) x
   | PairArgType _ -> app_pair (subst_genarg subst) (subst_genarg subst) x
-  | ExtraArgType s -> lookup_genarg_subst s subst x
+  | ExtraArgType s ->
+      match tactic_genarg_level s with
+      | Some n -> 
+          (* Special treatment of tactic arguments *)
+          in_gen (globwit_tactic n)
+            (subst_tactic subst (out_gen (globwit_tactic n) x))
+      | None -> 
+          lookup_genarg_subst s subst x
 
 (***************************************************************************)
 (* Tactic registration *)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index d7bbb2a4..ff6ac41a 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacticals.ml 7909 2006-01-21 11:09:18Z herbelin $ *)
+(* $Id: tacticals.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
 
 open Pp
 open Util
@@ -119,13 +119,13 @@ 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)]; onconcl=false; concl_occs=[] }
+let onHyp id = { onhyps=Some[(([],id),InHyp)]; 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)) (pf_ids_of_hyps gls)
+        None -> List.map (fun id -> Some(([],id),InHyp)) (pf_ids_of_hyps gls)
       | Some l -> List.map (fun h -> Some h) l in
   if cl.onconcl then None::hyps else hyps
 
@@ -167,7 +167,7 @@ let nth_clause n gl =
 let clause_type cls gl =
   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 *)
 
@@ -217,7 +217,7 @@ 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
+  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/tactics.ml b/tactics/tactics.ml
index 1d97dc4f..4eaf0259 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactics.ml 8701 2006-04-12 08:07:35Z courtieu $ *)
+(* $Id: tactics.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
 
 open Pp
 open Util
@@ -147,7 +147,7 @@ type tactic_reduction = env -> evar_map -> constr -> constr
 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 =
   let (_,c, ty) = pf_get_hyp gl id in
   let redfun' = (*under_casts*) (pf_reduce redfun gl) in
   match c with
@@ -967,19 +967,21 @@ let quantify lconstr =
    the left of each x1, ...).
 *)
 
-
+let out_arg = function
+  | ArgVar _ -> anomaly "Unevaluated or_var variable"
+  | ArgArg x -> x
 
 let occurrences_of_hyp id cls =
   let rec hyp_occ = function
       [] -> None
-    | (id',occs,hl)::_ when id=id' -> Some occs
+    | ((occs,id'),hl)::_ when id=id' -> Some (List.map out_arg 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
+  if cls.onconcl then Some (List.map out_arg cls.concl_occs) else None
 
 let in_every_hyp cls = (cls.onhyps=None)
 
@@ -1001,7 +1003,7 @@ let letin_abstract id c occs gl =
 		then raise (RefinerError (DoesNotOccurIn (c,hyp)))
 		else raise Not_found
               else 
-		(subst1_decl (mkVar id) newdecl, true)
+		(subst1_named_decl (mkVar id) newdecl, true)
 	with Not_found -> 
 	  (d,List.exists
 	      (fun ((id,_,_),dep) -> dep && occur_var_in_decl env id d) ctxt)
@@ -1053,7 +1055,7 @@ let letin_abstract id c occs gl =
 	    then raise (RefinerError (DoesNotOccurIn (c,hyp)))
 	    else depdecls
           else 
-	    (subst1_decl (mkVar id) newdecl)::depdecls in 
+	    (subst1_named_decl (mkVar id) newdecl)::depdecls in 
   let depdecls = fold_named_context compute_dependency env ~init:[] in
   let ccl = match occurrences_of_goal occs with
     | None -> pf_concl gl
@@ -1081,9 +1083,9 @@ let forward usetac ipat c gl =
   match usetac with
   | None -> 
       let t = refresh_universes (pf_type_of gl c) in
-      tclTHENS (assert_as true ipat t) [exact_no_check c; tclIDTAC] gl
+      tclTHENFIRST (assert_as true ipat t) (exact_no_check c) gl
   | Some tac -> 
-      tclTHENS (assert_as true ipat c) [tac; tclIDTAC] gl
+      tclTHENFIRST (assert_as true ipat c) tac gl
 
 (*****************************)
 (* High-level induction      *)
@@ -2004,7 +2006,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
@@ -2191,7 +2193,7 @@ let dAnd cls =
   onClauses
     (function
       | None    -> simplest_split
-      | Some (id,_,_) -> andE id)
+      | Some ((_,id),_) -> andE id)
     cls
 
 let orE id gl =
@@ -2205,7 +2207,7 @@ let orE id gl =
 let dorE b cls =
   onClauses
     (function
-      | (Some (id,_,_)) -> orE id
+      | (Some ((_,id),_)) -> orE id
       |  None     -> (if b then right else left) NoBindings)
     cls
 
@@ -2225,7 +2227,7 @@ let dImp cls =
   onClauses
     (function
       | None    -> intro
-      | Some (id,_,_) -> impE id)
+      | Some ((_,id),_) -> impE id)
     cls
 
 (************************************************)
@@ -2300,7 +2302,7 @@ let intros_symmetry =
   onClauses
     (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 5d04da9a..aaacee8f 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tactics.mli 8698 2006-04-11 15:12:48Z jforest $ i*)
+(*i $Id: tactics.mli 8878 2006-05-30 16:44:25Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -115,8 +115,8 @@ 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_in_concl   : tactic_reduction * cast_kind -> tactic
-val change_in_concl   : constr occurrences option -> constr -> tactic
-val change_in_hyp     : constr occurrences option -> constr -> hyp_location ->
+val change_in_concl   : (int list * constr) option -> constr -> tactic
+val change_in_hyp     : (int list * constr) option -> constr -> hyp_location ->
   tactic
 val red_in_concl      : tactic
 val red_in_hyp        : hyp_location        -> tactic
@@ -139,7 +139,7 @@ val unfold_option     :
     -> tactic
 val reduce            : red_expr -> clause -> tactic
 val change            :
-  constr occurrences option -> constr -> clause -> tactic
+  (int list * constr) option -> constr -> clause -> tactic
 
 val unfold_constr     : global_reference -> tactic
 val pattern_option  : (int list * constr) list -> simple_clause -> tactic