Imported Upstream version 8.1~gammaupstream/8.1.gamma

25 files changed, 3356 insertions, 786 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 7c1c375b..3cd1591d 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: auto.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
+(* $Id: auto.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
 
 open Pp
 open Util
@@ -192,7 +192,10 @@ let make_exact_entry (c,cty) =
 	   { pri=0; pat=None; code=Give_exact c })
 
 let dummy_goal =
-  {it={evar_hyps=empty_named_context_val;evar_concl=mkProp;evar_body=Evar_empty};
+  {it={evar_hyps=empty_named_context_val;
+       evar_concl=mkProp;
+       evar_body=Evar_empty;
+       evar_extra=None};
    sigma=Evd.empty}
 
 let make_apply_entry env sigma (eapply,verbose) (c,cty) =
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index ceeb4763..872b8697 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: autorewrite.ml 8114 2006-03-02 18:09:27Z herbelin $ *)
+(* $Id: autorewrite.ml 9157 2006-09-21 15:10:08Z herbelin $ *)
 
 open Equality
 open Hipattern
@@ -60,11 +60,11 @@ type raw_rew_rule = constr * bool * raw_tactic_expr
 
 (* Applies all the rules of one base *)
 let one_base general_rewrite_maybe_in tac_main bas =
-  let lrul = 
-    try 
+  let lrul =
+    try
       Stringmap.find bas !rewtab
-    with Not_found -> 
-      errorlabstrm "AutoRewrite" 
+    with Not_found ->
+      errorlabstrm "AutoRewrite"
         (str ("Rewriting base "^(bas)^" does not exist"))
   in
   let lrul = List.map (fun (c,_,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrul in
@@ -74,16 +74,19 @@ let one_base general_rewrite_maybe_in tac_main bas =
 	  (tclTHENSFIRSTn (general_rewrite_maybe_in dir csr) [|tac_main|] tc)))
       tclIDTAC lrul))
 
+
+
 (* The AutoRewrite tactic *)
 let autorewrite tac_main lbas =
   tclREPEAT_MAIN (tclPROGRESS
     (List.fold_left (fun tac bas -> 
        tclTHEN tac (one_base general_rewrite tac_main bas)) tclIDTAC lbas))
 
-let autorewrite_in id tac_main lbas gl =
+let autorewrite_mutlti_in idl tac_main lbas : tactic =
+  fun gl -> 
  (* let's check at once if id exists (to raise the appropriate error) *)
- let _ = Tacmach.pf_get_hyp gl id in
- let general_rewrite_in =
+ let _ = List.map (Tacmach.pf_get_hyp gl) idl in
+ let general_rewrite_in id =
   let id = ref id in
   let to_be_cleared = ref false in
    fun dir cstr gl ->
@@ -117,10 +120,51 @@ let autorewrite_in id tac_main lbas gl =
           | _ -> assert false) (* there must be at least an hypothesis *)
      | _ -> assert false (* rewriting cannot complete a proof *)
  in
+ tclMAP (fun id -> 
   tclREPEAT_MAIN (tclPROGRESS
     (List.fold_left (fun tac bas -> 
-       tclTHEN tac (one_base general_rewrite_in tac_main bas)) tclIDTAC lbas))
-   gl
+       tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) tclIDTAC lbas)))
+   idl gl
+
+let autorewrite_in id = autorewrite_mutlti_in [id]
+
+let gen_auto_multi_rewrite tac_main lbas cl = 
+  let try_do_hyps treat_id l = 
+    autorewrite_mutlti_in (List.map treat_id l) tac_main lbas
+  in 
+  if cl.concl_occs <> [] then 
+    error "The \"at\" syntax isn't available yet for the autorewrite tactic"
+  else 
+    let compose_tac t1 t2 = 
+      match cl.onhyps with 
+	| Some [] -> t1 
+	| _ ->      tclTHENFIRST t1 t2
+    in
+    compose_tac
+	(if cl.onconcl then autorewrite tac_main lbas else tclIDTAC)
+	(match cl.onhyps with 
+	   | Some l -> try_do_hyps (fun ((_,id),_) -> id) l
+	   | None -> 
+	       fun gl -> 
+		 (* try to rewrite in all hypothesis 
+		    (except maybe the rewritten one) *)
+		 let ids =  Tacmach.pf_ids_of_hyps gl
+		 in try_do_hyps (fun id -> id)  ids gl)
+
+let auto_multi_rewrite = gen_auto_multi_rewrite Refiner.tclIDTAC
+
+let auto_multi_rewrite_with tac_main lbas cl gl = 
+  match cl.Tacexpr.onconcl,cl.Tacexpr.onhyps with 
+    | false,Some [_] | true,Some [] | false,Some [] ->   
+	(* autorewrite with .... in clause using tac n'est sur que 
+	   si clause reprensente soit le but soit UNE hypothse 
+	*)
+	gen_auto_multi_rewrite tac_main  lbas cl gl
+    | _ -> 
+	    Util.errorlabstrm "autorewrite" 
+	      (str "autorewrite .. in .. using can only be used either with a unique hypothesis or" ++
+		 str " on the conclusion")
+
 
 (* Functions necessary to the library object declaration *)
 let cache_hintrewrite (_,(rbase,lrl)) =
@@ -165,8 +209,8 @@ let classify_hintrewrite (_,x) = Libobject.Substitute x
 (* Declaration of the Hint Rewrite library object *)
 let (in_hintrewrite,out_hintrewrite)=
   Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with
-       Libobject.open_function = (fun i o -> if i=1 then cache_hintrewrite o);
        Libobject.cache_function = cache_hintrewrite;
+       Libobject.load_function = (fun _ -> cache_hintrewrite);
        Libobject.subst_function = subst_hintrewrite;
        Libobject.classify_function = classify_hintrewrite;
        Libobject.export_function = export_hintrewrite }
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 47d3c86a..f402a35d 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: autorewrite.mli 7034 2005-05-18 19:30:44Z sacerdot $ i*)
+(*i $Id: autorewrite.mli 9073 2006-08-22 08:54:29Z jforest $ i*)
 
 (*i*)
 open Tacmach
@@ -22,4 +22,9 @@ val add_rew_rules : string -> raw_rew_rule list -> unit
 val autorewrite : tactic -> string list -> tactic
 val autorewrite_in : Names.identifier -> tactic -> string list -> tactic
 
+
+val auto_multi_rewrite : string list -> Tacticals.clause -> tactic
+
+val auto_multi_rewrite_with : tactic -> string list -> Tacticals.clause -> tactic
+
 val print_rewrite_hintdb : string -> unit
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 0f274aae..eca16066 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: contradiction.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: contradiction.ml 9269 2006-10-24 13:01:55Z herbelin $ *)
 
 open Util
 open Term
@@ -22,6 +22,10 @@ open Rawterm
 (* Absurd *)
 
 let absurd c gls =
+  let env = pf_env gls and sigma = project gls in
+  let _,j = Coercion.Default.inh_coerce_to_sort dummy_loc env
+    (Evd.create_evar_defs sigma) (Retyping.get_judgment_of env sigma c) in
+  let c = j.Environ.utj_val in
   (tclTHENS
      (tclTHEN (elim_type (build_coq_False ())) (cut c)) 
      ([(tclTHENS
diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
new file mode 100644
index 00000000..8ace0a08
--- /dev/null
+++ b/tactics/decl_interp.ml
@@ -0,0 +1,429 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Util
+open Names
+open Topconstr
+open Tacinterp
+open Tacmach
+open Decl_expr
+open Decl_mode
+open Pretyping.Default
+open Rawterm
+open Term
+open Pp
+
+let raw_app (loc,hd,args) = if args =[] then hd else RApp(loc,hd,args) 
+
+let intern_justification globs = function
+    Automated l -> Automated (List.map (intern_constr globs) l)
+  | By_tactic tac -> By_tactic (intern_tactic globs tac) 
+
+let intern_statement intern_it globs st =
+  {st_label=st.st_label;
+   st_it=intern_it globs st.st_it}
+    
+let intern_constr_or_thesis globs = function
+    Thesis n -> Thesis n
+  | This c -> This (intern_constr globs c)
+
+let add_var id globs= 
+  let l1,l2=globs.ltacvars in
+    {globs with ltacvars= (id::l1),(id::l2)}
+
+let add_name nam globs=
+ match nam with 
+     Anonymous -> globs
+   | Name id -> add_var id globs
+
+let intern_hyp iconstr globs = function 
+    Hvar (loc,(id,topt)) -> add_var id globs,
+      Hvar (loc,(id,option_map (intern_constr globs) topt))
+  | Hprop st -> add_name st.st_label globs,
+      Hprop (intern_statement iconstr globs st)
+
+let intern_hyps iconstr globs hyps = 
+  snd (list_fold_map (intern_hyp iconstr) globs hyps)
+
+let intern_cut intern_it globs cut=
+ {cut_stat=intern_statement intern_it globs cut.cut_stat;
+  cut_by=intern_justification globs cut.cut_by}
+
+let intern_casee globs = function 
+    Real c -> Real (intern_constr globs c)
+  | Virtual cut -> Virtual (intern_cut intern_constr globs cut) 
+
+let intern_hyp_list args globs =
+  let intern_one globs (loc,(id,opttyp)) =
+    (add_var id globs),
+    (loc,(id,option_map (intern_constr globs) opttyp)) in
+  list_fold_map intern_one globs args 
+
+let intern_fundecl args body globs= 
+  let nglobs,nargs = intern_hyp_list args globs in
+    nargs,intern_constr nglobs body
+          
+let rec add_vars_of_simple_pattern globs = function
+    CPatAlias (loc,p,id) ->
+      add_vars_of_simple_pattern (add_var id globs) p
+(*      Stdpp.raise_with_loc loc 
+	(UserError ("simple_pattern",str "\"as\" is not allowed here"))*)
+  | CPatOr (loc, _)->
+      Stdpp.raise_with_loc loc 
+	(UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here"))
+  | CPatDelimiters (_,_,p) ->
+      add_vars_of_simple_pattern globs p
+  | CPatCstr (_,_,pl) | CPatNotation(_,_,pl) ->
+      List.fold_left add_vars_of_simple_pattern globs pl
+  | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs
+  |  _  -> globs 
+
+let rec intern_bare_proof_instr globs = function
+    Pthus i -> Pthus (intern_bare_proof_instr globs i)
+  | Pthen i -> Pthen (intern_bare_proof_instr globs i)
+  | Phence i -> Phence (intern_bare_proof_instr globs i)
+  | Pcut c -> Pcut (intern_cut intern_constr_or_thesis globs c) 
+  | Prew (s,c) -> Prew (s,intern_cut intern_constr globs c) 
+  | Psuppose hyps -> Psuppose (intern_hyps intern_constr globs hyps)
+  | Pcase (params,pat,hyps) -> 
+      let nglobs,nparams = intern_hyp_list params globs in
+      let nnglobs= add_vars_of_simple_pattern nglobs pat in
+      let nhyps = intern_hyps intern_constr_or_thesis nnglobs hyps in
+	Pcase (nparams,pat,nhyps) 
+  | Ptake witl -> Ptake (List.map (intern_constr globs) witl)
+  | Pconsider (c,hyps) -> Pconsider (intern_constr globs c,
+				      intern_hyps intern_constr globs hyps)
+  | Pper (et,c) -> Pper (et,intern_casee globs c)
+  | Pend bt -> Pend bt
+  | Pescape -> Pescape
+  | Passume hyps -> Passume (intern_hyps intern_constr globs hyps)
+  | Pgiven hyps -> Pgiven (intern_hyps intern_constr globs hyps)
+  | Plet hyps -> Plet (intern_hyps intern_constr globs hyps)
+  | Pclaim st -> Pclaim (intern_statement intern_constr globs st)
+  | Pfocus st -> Pfocus (intern_statement intern_constr globs st)
+  | Pdefine (id,args,body) -> 
+      let nargs,nbody = intern_fundecl args body globs in
+	Pdefine (id,nargs,nbody)
+  | Pcast (id,typ) ->
+      Pcast (id,intern_constr globs typ)
+
+let rec intern_proof_instr globs instr=
+  {emph = instr.emph;
+   instr = intern_bare_proof_instr globs instr.instr}
+
+let interp_justification env sigma  = function
+    Automated l -> 
+      Automated (List.map (fun c ->understand env sigma (fst c)) l)
+  | By_tactic tac -> By_tactic tac 
+
+let interp_constr check_sort env sigma c = 
+  if check_sort then 
+    understand_type env sigma (fst c) 
+  else 
+    understand env sigma (fst c)
+
+let special_whd env =
+  let infos=Closure.create_clos_infos Closure.betadeltaiota env in
+    (fun t -> Closure.whd_val infos (Closure.inject t))
+
+let _eq = Libnames.constr_of_reference (Coqlib.glob_eq)
+
+let decompose_eq env id =
+  let typ = Environ.named_type id env in
+  let whd = special_whd env typ in
+    match kind_of_term whd with
+	App (f,args)->
+	  if eq_constr f _eq && (Array.length args)=3 
+	  then args.(0)
+	  else error "previous step is not an equality"
+      | _ -> error "previous step is not an equality"
+
+let get_eq_typ info env =
+  let last_id = 	    
+    match info.pm_last with
+	Anonymous -> error "no previous equality"
+      | Name id -> id in
+  let typ = decompose_eq env last_id in  
+    typ
+
+let interp_constr_in_type typ env sigma c =
+  understand env sigma (fst c) ~expected_type:typ
+
+let interp_statement interp_it env sigma st =
+  {st_label=st.st_label;
+   st_it=interp_it env sigma st.st_it}
+	
+let interp_constr_or_thesis check_sort env sigma = function
+    Thesis n -> Thesis n
+  | This c -> This (interp_constr check_sort env sigma c)
+
+let type_tester_var body typ = 
+  raw_app(dummy_loc,
+       RLambda(dummy_loc,Anonymous,typ,
+	       RSort (dummy_loc,RProp Null)),body)
+
+let abstract_one_hyp inject h raw = 
+  match h with 
+      Hvar (loc,(id,None)) ->  
+	RProd (dummy_loc,Name id, RHole (loc,Evd.BinderType (Name id)), raw)
+    | Hvar (loc,(id,Some typ)) ->  
+	RProd (dummy_loc,Name id,fst typ, raw)
+    | Hprop st -> 
+	RProd (dummy_loc,st.st_label,inject st.st_it, raw)
+
+let rawconstr_of_hyps inject hyps = 
+  List.fold_right (abstract_one_hyp inject) hyps (RSort (dummy_loc,RProp Null))
+  
+let rec match_hyps blend names constr = function 
+    [] -> []
+  | hyp::q -> 
+      let (name,typ,body)=destProd constr in
+      let st= {st_label=name;st_it=substl names typ} in
+      let qnames=
+	match name with
+	    Anonymous -> mkMeta 0 :: names
+	  | Name id -> mkVar id :: names in
+      let qhyp = match hyp with
+	  Hprop st' -> Hprop (blend st st')
+	| Hvar _ -> Hvar st in
+	qhyp::(match_hyps blend qnames body q)
+
+let interp_hyps_gen inject blend env sigma hyps = 
+  let constr=understand env sigma (rawconstr_of_hyps inject hyps) in
+    match_hyps blend [] constr hyps
+
+let interp_hyps = interp_hyps_gen fst (fun x _ -> x)
+
+let dummy_prefix= id_of_string "__"
+
+let rec deanonymize ids = 
+  function 
+      PatVar (loc,Anonymous) -> 
+	let (found,known) = !ids in
+	let new_id=Nameops.next_ident_away dummy_prefix known in
+	let _= ids:= (loc,new_id) :: found , new_id :: known in
+	  PatVar (loc,Name new_id)
+    | PatVar (loc,Name id) as pat -> 
+	let (found,known) = !ids in
+	let _= ids:= (loc,id) :: found , known in
+	  pat
+    | PatCstr(loc,cstr,lpat,nam) -> 
+	PatCstr(loc,cstr,List.map (deanonymize ids) lpat,nam)
+
+let rec raw_of_pat =
+  function 
+      PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable" 
+    | PatVar (loc,Name id) -> 
+	  RVar (loc,id)
+    | PatCstr(loc,((ind,_) as cstr),lpat,_) -> 
+	let mind= fst (Global.lookup_inductive ind) in
+	let rec add_params n q =
+	  if n<=0 then q else
+	    add_params (pred n) (RHole(dummy_loc,
+				       Evd.TomatchTypeParameter(ind,n))::q) in
+	    let args = List.map raw_of_pat lpat in 
+	      raw_app(loc,RRef(dummy_loc,Libnames.ConstructRef cstr),
+		   add_params mind.Declarations.mind_nparams args) 
+			 
+let prod_one_hyp = function
+    (loc,(id,None)) ->
+      (fun raw ->  
+	 RProd (dummy_loc,Name id, 
+		RHole (loc,Evd.BinderType (Name id)), raw))
+  | (loc,(id,Some typ)) -> 
+      (fun raw ->  
+	 RProd (dummy_loc,Name id,fst typ, raw))
+
+let prod_one_id (loc,id) raw =
+  RProd (dummy_loc,Name id,
+	 RHole (loc,Evd.BinderType (Name id)), raw)
+
+let let_in_one_alias (id,pat) raw =
+  RLetIn (dummy_loc,Name id,raw_of_pat pat, raw)
+
+let rec bind_primary_aliases map pat =
+  match pat with 
+      PatVar (_,_) -> map
+    | PatCstr(loc,_,lpat,nam) ->
+	let map1 =
+	  match nam with 
+	      Anonymous -> map
+	    | Name id -> (id,pat)::map 
+	in
+	  List.fold_left bind_primary_aliases map1 lpat
+
+let bind_secondary_aliases map subst =
+  List.fold_left (fun map (ids,idp) -> (ids,List.assoc idp map)::map) map subst
+
+let bind_aliases patvars subst patt =
+  let map = bind_primary_aliases [] patt in
+  let map1 = bind_secondary_aliases map subst in
+  List.rev map1
+
+let interp_pattern env pat_expr = 
+  let patvars,pats = Constrintern.intern_pattern env pat_expr in
+    match pats with 
+	[] -> anomaly "empty pattern list"
+      | [subst,patt] ->
+	  (patvars,bind_aliases patvars subst patt,patt)
+      | _  -> anomaly "undetected disjunctive pattern"
+
+let rec match_args dest names constr = function 
+    [] -> [],names,substl names constr
+  | _::q -> 
+      let (name,typ,body)=dest constr in
+      let st={st_label=name;st_it=substl names typ} in
+      let qnames=
+	match name with
+	    Anonymous -> assert  false
+	  | Name id -> mkVar id :: names in
+      let args,bnames,body = match_args dest qnames body q in
+	st::args,bnames,body
+
+let rec match_aliases names constr = function 
+    [] -> [],names,substl names constr
+  | _::q -> 
+      let (name,c,typ,body)=destLetIn constr in
+      let st={st_label=name;st_it=(substl names c,substl names typ)} in
+      let qnames=
+	match name with
+	    Anonymous -> assert false
+	  | Name id -> mkVar id :: names in
+      let args,bnames,body = match_aliases qnames body q in
+	st::args,bnames,body
+
+let detype_ground c = Detyping.detype false [] [] c
+
+let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
+  let et,pinfo =
+    match info.pm_stack with
+	Per(et,pi,_,_)::_ -> et,pi
+      | _ -> error "No proof per cases/induction/inversion in progress." in
+  let mib,oib=Global.lookup_inductive  pinfo.per_ind in
+  let num_params = pinfo.per_nparams in
+  let _ = 
+    let expected = mib.Declarations.mind_nparams - num_params in
+      if List.length params <> expected then
+	errorlabstrm "suppose it is" 
+	  (str "Wrong number of extra arguments : " ++ 
+	     (if expected = 0 then str "none" else int expected) ++ 
+	     str "expected") in
+  let app_ind =
+    let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in
+    let rparams = List.map detype_ground pinfo.per_params in 
+    let rparams_rec = 
+      List.map 
+	(fun (loc,(id,_)) -> 
+	   RVar (loc,id)) params in 
+    let dum_args= 
+      list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark))
+	oib.Declarations.mind_nrealargs in
+      raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in
+  let pat_vars,aliases,patt = interp_pattern env pat in
+  let inject = function
+      Thesis (Plain) -> Rawterm.RSort(dummy_loc,RProp Null)
+    | Thesis (Sub n) ->
+	error "thesis[_] is not allowed here"
+    | Thesis (For rec_occ) ->
+	if not (List.mem rec_occ pat_vars) then 
+	  errorlabstrm "suppose it is" 
+	    (str "Variable " ++ Nameops.pr_id rec_occ ++ 
+	       str " does not occur in pattern.");
+	Rawterm.RSort(dummy_loc,RProp Null)
+    | This (c,_) -> c in
+  let term1 = rawconstr_of_hyps inject hyps in
+  let loc_ids,npatt =
+    let rids=ref ([],pat_vars) in
+    let npatt= deanonymize rids patt in 
+      List.rev (fst !rids),npatt in
+  let term2 =
+    RLetIn(dummy_loc,Anonymous,
+	   RCast(dummy_loc,raw_of_pat npatt,
+		 CastConv DEFAULTcast,app_ind),term1) in
+  let term3=List.fold_right let_in_one_alias aliases term2 in  
+  let term4=List.fold_right prod_one_id loc_ids term3 in
+  let term5=List.fold_right prod_one_hyp params term4 in
+  let constr = understand  sigma env term5 in
+  let tparams,nam4,rest4 = match_args destProd [] constr params in
+  let tpatvars,nam3,rest3 = match_args destProd nam4 rest4 loc_ids in
+  let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in
+  let (_,pat_pat,pat_typ,rest1) = destLetIn rest2 in
+  let blend  st st' =
+    match st'.st_it with 
+	Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label} 
+      | This _ -> {st_it = This st.st_it;st_label=st.st_label} in
+  let thyps = match_hyps blend nam2 (Termops.pop rest1) hyps in
+    tparams,{pat_vars=tpatvars;
+	     pat_aliases=taliases;
+	     pat_constr=pat_pat;
+	     pat_typ=pat_typ;
+	     pat_pat=patt;
+	     pat_expr=pat},thyps
+
+let interp_cut interp_it env sigma cut=
+ {cut_stat=interp_statement interp_it env sigma cut.cut_stat;
+  cut_by=interp_justification env sigma cut.cut_by}
+
+let interp_casee env sigma = function 
+    Real c -> Real (understand env sigma (fst c))
+  | Virtual cut -> Virtual (interp_cut (interp_constr true) env sigma cut) 
+
+let abstract_one_arg = function
+    (loc,(id,None)) ->
+      (fun raw ->  
+	 RLambda (dummy_loc,Name id, 
+		RHole (loc,Evd.BinderType (Name id)), raw))
+  | (loc,(id,Some typ)) -> 
+      (fun raw ->  
+	 RLambda (dummy_loc,Name id,fst typ, raw))
+
+let rawconstr_of_fun args body = 
+  List.fold_right abstract_one_arg args (fst body)
+
+let interp_fun env sigma args body = 
+  let constr=understand env sigma (rawconstr_of_fun args body) in
+    match_args destLambda [] constr args
+
+let rec interp_bare_proof_instr info sigma env = function
+    Pthus i -> Pthus (interp_bare_proof_instr info sigma env i)
+  | Pthen i -> Pthen (interp_bare_proof_instr info sigma env i)
+  | Phence i -> Phence (interp_bare_proof_instr info sigma env i)
+  | Pcut c -> Pcut (interp_cut (interp_constr_or_thesis true) sigma env c) 
+  | Prew (s,c) -> Prew (s,interp_cut 
+			  (interp_constr_in_type (get_eq_typ info env))
+			  sigma env c) 
+  | Psuppose hyps -> Psuppose (interp_hyps sigma env hyps)
+  | Pcase (params,pat,hyps) -> 
+      let tparams,tpat,thyps = interp_cases info env sigma params pat hyps in 
+	Pcase (tparams,tpat,thyps)
+  | Ptake witl -> 
+      Ptake (List.map (fun c -> understand sigma env (fst c)) witl)
+  | Pconsider (c,hyps) -> Pconsider (interp_constr false sigma env c,
+				     interp_hyps sigma env hyps)
+  | Pper (et,c) -> Pper (et,interp_casee sigma env c)
+  | Pend bt -> Pend bt
+  | Pescape -> Pescape
+  | Passume hyps -> Passume (interp_hyps sigma env hyps)
+  | Pgiven hyps -> Pgiven (interp_hyps sigma env hyps)
+  | Plet hyps -> Plet (interp_hyps sigma env hyps)
+  | Pclaim st -> Pclaim (interp_statement (interp_constr true) sigma env st)
+  | Pfocus st -> Pfocus (interp_statement (interp_constr true) sigma env st)
+  | Pdefine (id,args,body) -> 
+      let nargs,_,nbody = interp_fun sigma env args body in
+	Pdefine (id,nargs,nbody)
+  | Pcast (id,typ) -> 
+      Pcast(id,interp_constr true sigma env typ)
+
+let rec interp_proof_instr info sigma env instr=
+  {emph = instr.emph;
+   instr = interp_bare_proof_instr info sigma env instr.instr}
+ 
+
+
diff --git a/tactics/decl_interp.mli b/tactics/decl_interp.mli
new file mode 100644
index 00000000..08d97646
--- /dev/null
+++ b/tactics/decl_interp.mli
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Tacinterp
+open Decl_expr
+open Mod_subst
+
+
+val intern_proof_instr : glob_sign -> raw_proof_instr -> glob_proof_instr
+val interp_proof_instr : Decl_mode.pm_info ->
+  Evd.evar_map -> Environ.env -> glob_proof_instr -> proof_instr
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
new file mode 100644
index 00000000..e7acd6d6
--- /dev/null
+++ b/tactics/decl_proof_instr.ml
@@ -0,0 +1,1476 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Util
+open Pp
+open Evd
+
+open Refiner
+open Proof_type
+open Proof_trees
+open Tacmach
+open Tacinterp
+open Decl_expr
+open Decl_mode
+open Decl_interp
+open Rawterm
+open Names
+open Declarations
+open Tactics
+open Tacticals
+open Term
+open Termops
+open Reductionops
+open Goptions
+
+(* Strictness option *)
+
+let get_its_info gls = get_info gls.it
+
+let get_strictness,set_strictness = 
+  let strictness = ref false in
+    (fun () -> (!strictness)),(fun b -> strictness:=b)
+
+let _ =
+  declare_bool_option 
+    { optsync  = true;
+      optname  = "strict mode";
+      optkey   = (SecondaryTable ("Strict","Proofs"));
+      optread  = get_strictness;
+      optwrite = set_strictness }
+
+let tcl_change_info_gen info_gen = 
+  (fun gls ->
+  let gl =sig_it gls in  
+    {it=[{gl with evar_extra=info_gen}];sigma=sig_sig gls}, 
+  function 
+      [pftree] ->
+	{pftree with
+	   goal=gl;
+	   ref=Some (Change_evars,[pftree])} 
+    | _ -> anomaly "change_info : Wrong number of subtrees")
+
+let tcl_change_info info gls =  tcl_change_info_gen (Some (pm_in info)) gls
+
+let tcl_erase_info gls =  tcl_change_info_gen None gls
+
+let special_whd gl=
+  let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in
+    (fun t -> Closure.whd_val infos (Closure.inject t))
+
+let special_nf gl=
+  let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in
+    (fun t -> Closure.norm_val infos (Closure.inject t))
+
+let is_good_inductive env ind =
+  let mib,oib = Inductive.lookup_mind_specif env ind in
+    oib.mind_nrealargs = 0 && not (Inductiveops.mis_is_recursive (ind,mib,oib))
+
+let check_not_per pts =
+  if not (Proof_trees.is_complete_proof (proof_of_pftreestate pts)) then
+    match get_stack pts with
+	Per (_,_,_,_)::_ -> 
+	  error "You are inside a proof per cases/induction.\n\
+Please \"suppose\" something or \"end\" it now."
+      | _ -> ()
+
+let get_thesis gls0 = 
+ let info = get_its_info gls0 in  
+    match info.pm_subgoals with
+	[m,thesis] -> thesis
+      | _ -> error "Thesis is split"
+
+let mk_evd metalist gls =
+  let evd0= create_evar_defs (sig_sig gls) in
+  let add_one (meta,typ) evd = 
+    meta_declare meta typ evd in
+    List.fold_right add_one metalist evd0
+	  
+(* start a proof *)
+
+let start_proof_tac gls=
+  let gl=sig_it gls in
+  let info={pm_last=Anonymous;
+	    pm_partial_goal=mkMeta 1; 
+	    pm_hyps= 
+      begin
+	let hyps = pf_ids_of_hyps gls in
+	  List.fold_right Idset.add hyps Idset.empty
+      end; 
+	    pm_subgoals= [1,gl.evar_concl];
+	    pm_stack=[]} in
+    {it=[{gl with evar_extra=Some (pm_in info)}];sigma=sig_sig gls}, 
+  function 
+      [pftree] ->
+	{pftree with
+	   goal=gl;
+	   ref=Some (Decl_proof true,[pftree])} 
+    | _ -> anomaly "Dem : Wrong number of subtrees"
+
+let go_to_proof_mode () = 
+  Pfedit.mutate 
+    (fun pts -> nth_unproven 1 (solve_pftreestate start_proof_tac pts))
+
+(* closing gaps *)
+
+let daimon_tac gls =
+  set_daimon_flag ();
+  ({it=[];sigma=sig_sig gls}, 
+   function 
+       [] ->
+	 {open_subgoals=0;
+	    goal=sig_it gls;
+	    ref=Some (Daimon,[])} 
+     | _ -> anomaly "Daimon: Wrong number of subtrees")
+    
+let daimon _ pftree =
+  set_daimon_flag ();
+  {pftree with
+     open_subgoals=0;
+     ref=Some (Daimon,[])}
+
+let daimon_subtree = map_pftreestate (fun _ ->  frontier_mapi daimon )
+
+(* marking closed blocks *)
+
+let rec is_focussing_instr = function
+    Pthus i | Pthen i | Phence i -> is_focussing_instr i
+  | Pescape | Pper _ | Pclaim _ | Pfocus _ 
+  | Psuppose _ | Pcase (_,_,_)  -> true
+  | _ -> false
+
+let mark_rule_as_done = function
+    Decl_proof true -> Decl_proof false
+  | Decl_proof false ->
+      anomaly "already marked as done"
+  | Nested(Proof_instr (lock_focus,instr),spfl) -> 
+      if lock_focus then
+	Nested(Proof_instr (false,instr),spfl)
+      else
+	anomaly "already marked as done"
+  | _ -> anomaly "mark_rule_as_done"
+
+let mark_proof_tree_as_done pt =
+  match pt.ref with
+      None -> anomaly "mark_proof_tree_as_done"
+    | Some (r,spfl) -> 
+	{pt with ref= Some (mark_rule_as_done r,spfl)}
+
+let mark_as_done pts = 
+  map_pftreestate 
+    (fun _ -> mark_proof_tree_as_done) 
+    (traverse 0 pts) 
+
+(* post-instruction focus management *)
+
+let goto_current_focus pts = up_until_matching_rule is_focussing_command pts
+
+let goto_current_focus_or_top pts = 
+  try 
+    up_until_matching_rule is_focussing_command pts
+  with Not_found -> top_of_tree pts
+
+(* return *)
+
+let close_tactic_mode pts =
+    let pts1=  
+      try goto_current_focus pts 
+      with Not_found -> 
+	error "\"return\" cannot be used outside of Declarative Proof Mode" in
+    let pts2 = daimon_subtree pts1 in
+    let pts3 = mark_as_done pts2 in 
+      goto_current_focus pts3 
+	  
+let return_from_tactic_mode () = Pfedit.mutate close_tactic_mode
+
+(* end proof/claim *)
+
+let close_block bt pts =
+  let stack =
+    if Proof_trees.is_complete_proof (proof_of_pftreestate pts) then
+      get_top_stack pts
+    else
+      get_stack pts in
+    match bt,stack with
+	B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> 
+	  daimon_subtree (goto_current_focus pts)
+      | _, Claim::_ -> 
+	  error "\"end claim\" expected" 
+      | _, Focus_claim::_ -> 
+	  error "\"end focus\" expected" 
+      | _, [] ->
+ 	  error "\"end proof\" expected" 
+      | _, (Per (et,_,_,_)::_|Suppose_case::Per (et,_,_,_)::_) ->
+	  begin
+	    match et with
+		ET_Case_analysis -> error "\"end cases\" expected"
+	      | ET_Induction ->  error "\"end induction\" expected"
+	  end
+      | _,_ -> anomaly "lonely suppose on stack"
+
+(* utility for suppose / suppose it is *)
+
+let close_previous_case pts = 
+  if 
+    Proof_trees.is_complete_proof (proof_of_pftreestate pts) 
+  then
+    match get_top_stack pts with
+	Per (et,_,_,_) :: _ -> anomaly "Weird case occured ..."  
+      | Suppose_case :: Per (et,_,_,_) :: _ -> 
+	  goto_current_focus (mark_as_done pts)
+      | _ -> error "Not inside a proof per cases or induction."   
+  else
+    match get_stack pts with
+	Per (et,_,_,_) :: _ -> pts 
+      | Suppose_case :: Per (et,_,_,_) :: _ ->
+	  goto_current_focus (mark_as_done (daimon_subtree pts))
+      | _ -> error "Not inside a proof per cases or induction."
+
+(* Proof instructions *)
+
+(* automation *)
+
+let filter_hyps f gls =
+  let filter_aux (id,_,_) = 
+    if f id then 
+      tclIDTAC
+    else 
+      tclTRY (clear [id])  in
+    tclMAP filter_aux (Environ.named_context_of_val gls.it.evar_hyps) gls
+
+let local_hyp_prefix = id_of_string "___"
+
+let add_justification_hyps keep items gls =
+  let add_aux c gls=
+    match kind_of_term c with 
+	Var id -> 
+	  keep:=Idset.add id !keep;
+	  tclIDTAC gls 
+      | _ -> 
+	  let id=pf_get_new_id local_hyp_prefix gls in 
+	    keep:=Idset.add id !keep; 
+	    letin_tac false (Names.Name id) c Tacexpr.nowhere gls in 
+    tclMAP add_aux items gls   
+
+let apply_to_prepared_goal items kont gls =
+  let tokeep = ref Idset.empty in
+  let auxres = add_justification_hyps tokeep items gls in
+   tclTHENLIST
+     [ (fun _ -> auxres);
+       filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep);
+       kont ] gls
+
+let my_automation_tac = ref 
+  (fun gls -> anomaly "No automation registered")
+
+let register_automation_tac tac = my_automation_tac:= tac
+
+let automation_tac gls = !my_automation_tac gls
+
+let justification tac gls= 
+    tclORELSE 
+      (tclSOLVE [tac]) 
+      (fun gls -> 
+	 if get_strictness () then 
+	   error "insufficient justification" 
+	 else
+	   begin
+	     msgnl (str "Warning: insufficient justification");  
+	     daimon_tac gls
+	   end) gls
+
+let default_justification items gls=
+  justification (apply_to_prepared_goal items automation_tac) gls
+
+(* code for have/then/thus/hence *)
+
+type stackd_elt =
+{se_meta:metavariable;
+ se_type:types;
+ se_last_meta:metavariable;
+ se_meta_list:(metavariable*types) list;
+ se_evd: evar_defs}
+
+let rec replace_in_list m l = function
+    [] -> raise Not_found
+  | c::q -> if m=fst c then l@q else c::replace_in_list m l q
+
+let enstack_subsubgoals env se stack gls=
+  let hd,params = decompose_app (special_whd gls se.se_type) in
+    match kind_of_term hd with
+	Ind ind when is_good_inductive env ind ->
+	  let mib,oib=
+	    Inductive.lookup_mind_specif env ind in
+          let gentypes=
+            Inductive.arities_of_constructors ind (mib,oib) in
+	  let process i gentyp = 
+	    let constructor = mkConstruct(ind,succ i) 
+	      (* constructors numbering*) in
+	    let appterm = applist (constructor,params) in
+	    let apptype = Term.prod_applist gentyp params in
+	    let rc,_ = Reduction.dest_prod env apptype in
+	    let rec meta_aux last lenv = function 
+		[] -> (last,lenv,[])
+	      | (nam,_,typ)::q ->
+		  let nlast=succ last in
+		  let (llast,holes,metas) =
+		    meta_aux nlast (mkMeta nlast :: lenv) q in
+		    (llast,holes,(nlast,special_nf gls (substl lenv typ))::metas) in
+	    let (nlast,holes,nmetas) = 
+		meta_aux se.se_last_meta [] (List.rev rc) in
+	    let refiner = applist (appterm,List.rev holes) in
+	    let evd = meta_assign se.se_meta refiner se.se_evd in
+	    let ncreated = replace_in_list 
+	      se.se_meta nmetas se.se_meta_list in
+	    let evd0 = List.fold_left 
+	      (fun evd (m,typ) -> meta_declare m typ evd) evd nmetas in  
+	      List.iter (fun (m,typ) -> 
+			   Stack.push 
+			     {se_meta=m;
+			      se_type=typ;
+			      se_evd=evd0;
+			      se_meta_list=ncreated;
+			      se_last_meta=nlast} stack) (List.rev nmetas) 
+	  in
+	    Array.iteri process gentypes
+      | _ -> ()
+
+let find_subsubgoal env c ctyp skip evd metas gls =
+  let stack = Stack.create () in
+  let max_meta = 
+    List.fold_left (fun a (m,_) -> max a m) 0 metas in
+  let _ = 
+    List.iter (fun (m,typ) -> 
+		 Stack.push 
+		   {se_meta=m;
+		    se_type=typ;
+		    se_last_meta=max_meta;
+		    se_meta_list=metas;
+		    se_evd=evd} stack) (List.rev metas) in
+  let rec dfs n = 
+    let se = Stack.pop stack in
+      try 
+	let unifier = 
+	  Unification.w_unify true env Reduction.CUMUL 
+	    ctyp se.se_type se.se_evd in
+	  if n <= 0 then 
+	      {se with se_evd=meta_assign se.se_meta c unifier}	  
+	  else
+	      dfs (pred n)
+      with _ -> 
+	begin
+	  enstack_subsubgoals env se stack gls;
+	  dfs n
+	end in
+  let nse= try dfs skip with Stack.Empty -> raise Not_found in
+    nse.se_meta_list,nse.se_evd
+
+let rec nf_list evd = 
+  function
+      [] -> []  
+    | (m,typ)::others -> 
+	if meta_defined evd m then 
+	    nf_list evd others
+	else
+	  (m,nf_meta evd typ)::nf_list evd others
+
+
+let rec max_linear_context meta_one c =
+  if !meta_one = None then
+     if isMeta c then
+       	begin
+	  meta_one:= Some c;
+          mkMeta 1
+	end
+     else
+       try
+	 map_constr (max_linear_context meta_one) c
+       with Not_found -> 
+	 begin
+	   meta_one:= Some c;
+           mkMeta 1
+	 end
+  else   
+    if isMeta c then 
+      raise Not_found
+    else
+      map_constr (max_linear_context meta_one) c
+
+let thus_tac c ctyp gls =  
+  let info = get_its_info gls in
+  let evd0 = mk_evd info.pm_subgoals gls in
+  let list,evd = 
+    try
+      find_subsubgoal (pf_env gls) c ctyp 0 evd0 info.pm_subgoals gls
+    with Not_found -> 
+      error "I could not relate this statement to the thesis" in
+  let nflist = nf_list evd list in
+  let nfgoal = nf_meta evd info.pm_partial_goal in
+(*  let _ = msgnl (str "Partial goal : " ++ 
+		   print_constr_env (pf_env gls) nfgoal) in *)
+  let rgl = ref None in
+  let refiner = max_linear_context rgl nfgoal in
+    match !rgl with
+	None -> exact_check refiner gls
+      | Some pgl when not (isMeta refiner) ->
+	  let ninfo={info with
+		       pm_partial_goal = pgl;
+		       pm_subgoals = nflist} in
+	    tclTHEN
+	      (Tactics.refine refiner)
+	      (tcl_change_info ninfo) 
+	      gls
+      | _ -> 
+	  let ninfo={info with
+		       pm_partial_goal = nfgoal;
+		       pm_subgoals = nflist} in
+	    tcl_change_info ninfo gls
+
+let anon_id_base = id_of_string "__" 
+
+
+let mk_stat_or_thesis info = function  
+    This c -> c
+  | Thesis (For _ ) -> 
+      error "\"thesis for ...\" is not applicable here" 
+  | Thesis (Sub n) ->
+      begin
+	try List.assoc n info.pm_subgoals 
+	with Not_found -> error "No such part in thesis."
+      end
+  | Thesis Plain ->   
+      match info.pm_subgoals with
+	  [_,c] -> c
+	| _ -> error 
+	    "\"thesis\" is split, please specify which part you refer to."
+			
+let instr_cut mkstat _thus _then cut gls0 = 
+  let info = get_its_info gls0 in  
+  let just_tac gls = 
+    match cut.cut_by with
+        Automated l ->	
+	  let elems = 
+	    if _then then
+	      match info.pm_last with
+		  Anonymous -> l
+		| Name id -> (mkVar id) ::l
+	    else l in
+	    default_justification elems gls
+      | By_tactic t -> 
+	  justification (Tacinterp.eval_tactic t) gls in
+  let c_id = match cut.cut_stat.st_label with 
+      Anonymous -> 
+	pf_get_new_id (id_of_string "_fact") gls0 
+    | Name id -> id in
+  let c_stat = mkstat info cut.cut_stat.st_it in
+  let thus_tac gls= 
+    if _thus then 
+      thus_tac (mkVar c_id) c_stat gls
+    else tclIDTAC gls in
+  let ninfo = {info with pm_last=Name c_id} in
+    tclTHENS (internal_cut c_id c_stat) 
+      [tclTHEN tcl_erase_info just_tac;
+       tclTHEN (tcl_change_info ninfo) thus_tac] gls0
+
+(* iterated equality *)
+let _eq = Libnames.constr_of_reference (Coqlib.glob_eq)
+
+let decompose_eq id gls =
+  let typ = pf_get_hyp_typ gls id in
+  let whd =  (special_whd gls typ) in
+    match kind_of_term whd with
+	App (f,args)->
+	  if eq_constr f _eq && (Array.length args)=3 
+	  then (args.(0),
+		args.(1), 
+		args.(2)) 
+	  else error "previous step is not an equality"
+      | _ -> error "previous step is not an equality"
+	  
+let instr_rew _thus rew_side cut gls0 = 
+  let info = get_its_info gls0 in
+  let last_id = 	    
+    match info.pm_last with
+	Anonymous -> error "no previous equality"
+      | Name id -> id in
+  let typ,lhs,rhs = decompose_eq last_id gls0 in  
+  let just_tac gls = 
+    match cut.cut_by with
+        Automated l ->	
+	  let elems = (mkVar last_id) :: l in
+	    default_justification elems gls
+      | By_tactic t -> 
+	  justification (Tacinterp.eval_tactic t) gls in
+  let c_id = match cut.cut_stat.st_label with 
+      Anonymous -> 
+	pf_get_new_id (id_of_string "_eq") gls0 
+    | Name id -> id in
+  let ninfo = {info with pm_last=Name c_id} in
+  let thus_tac new_eq gls= 
+    if _thus then 
+      thus_tac (mkVar c_id) new_eq gls
+    else tclIDTAC gls in
+    match rew_side with 
+	Lhs ->
+	  let new_eq = mkApp(_eq,[|typ;cut.cut_stat.st_it;rhs|]) in
+	    tclTHENS (internal_cut c_id new_eq) 
+	      [tclTHEN tcl_erase_info 
+		 (tclTHENS (transitivity lhs) 
+		    [just_tac;exact_check (mkVar last_id)]);
+	       tclTHEN (tcl_change_info ninfo) (thus_tac new_eq)] gls0
+      | Rhs ->
+	  let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in
+	    tclTHENS (internal_cut c_id new_eq) 
+	      [tclTHEN tcl_erase_info 
+		 (tclTHENS (transitivity rhs) 
+		    [exact_check (mkVar last_id);just_tac]);
+	       tclTHEN (tcl_change_info ninfo) (thus_tac new_eq)] gls0
+	      
+
+
+(* tactics for claim/focus *)
+
+let instr_claim _thus st gls0 = 
+  let info = get_its_info gls0 in  
+  let id = match st.st_label with 
+      Anonymous -> pf_get_new_id (id_of_string "_claim") gls0 
+    | Name id -> id in
+  let thus_tac gls= 
+    if _thus then 
+      thus_tac (mkVar id) st.st_it gls
+    else tclIDTAC gls in
+  let ninfo1 = {info with 
+		  pm_stack=
+      (if _thus then Focus_claim else Claim)::info.pm_stack;
+		  pm_partial_goal=mkMeta 1;
+	          pm_subgoals = [1,st.st_it]} in
+  let ninfo2 = {info with pm_last=Name id} in
+    tclTHENS (internal_cut id st.st_it) 
+      [tcl_change_info ninfo1;
+       tclTHEN (tcl_change_info ninfo2) thus_tac] gls0
+
+(* tactics for assume *)
+
+let reset_concl gls =
+  let info = get_its_info gls in
+    tcl_change_info 
+      {info with 
+	 pm_partial_goal=mkMeta 1;
+	 pm_subgoals= [1,gls.it.evar_concl]} gls
+
+let set_last id gls = 
+  let info = get_its_info gls in
+    tcl_change_info 
+      {info with 
+	 pm_last=Name id} gls
+
+let intro_pm id gls=
+  let info = get_its_info gls in
+    match info.pm_subgoals with
+	[(_,typ)] -> 
+	  tclTHEN (intro_mustbe_force id) reset_concl gls
+      | _ -> error "Goal is split"
+
+let push_intro_tac coerce nam gls = 
+      let hid =
+	match nam with 
+	    Anonymous -> pf_get_new_id (id_of_string "_hyp") gls 
+	  | Name id -> id in
+      let mark_id gls0 =
+	let info = get_its_info gls0 in
+	let ninfo = {info with 
+		       pm_last = Name hid;
+		       pm_hyps = Idset.add hid info.pm_hyps } in
+	  tcl_change_info ninfo gls0 in
+	tclTHENLIST 
+	  [intro_pm hid;
+	   coerce hid;
+	   mark_id]
+	  gls 
+
+let assume_tac hyps gls = 
+  List.fold_right 
+    (fun (Hvar st | Hprop st) -> 
+       tclTHEN 
+	 (push_intro_tac 
+	    (fun id -> 
+	       convert_hyp (id,None,st.st_it)) st.st_label))
+	 hyps tclIDTAC gls 
+
+let assume_hyps_or_theses hyps gls = 
+  List.fold_right 
+    (function 
+	 (Hvar {st_label=nam;st_it=c} | Hprop {st_label=nam;st_it=This c}) -> 
+	   tclTHEN 
+	     (push_intro_tac 
+		(fun id -> 
+		   convert_hyp (id,None,c)) nam)
+       | Hprop {st_label=nam;st_it=Thesis (tk)} -> 
+	   tclTHEN 
+	     (push_intro_tac 
+		(fun id -> tclIDTAC) nam))
+    hyps tclIDTAC gls 
+
+let assume_st hyps gls = 
+  List.fold_right 
+    (fun st -> 
+       tclTHEN 
+	 (push_intro_tac 
+	    (fun id -> convert_hyp (id,None,st.st_it)) st.st_label))
+	 hyps tclIDTAC gls 
+
+let assume_st_letin hyps gls = 
+  List.fold_right 
+    (fun st -> 
+       tclTHEN 
+	 (push_intro_tac 
+	    (fun id -> 
+	       convert_hyp (id,Some (fst st.st_it),snd st.st_it)) st.st_label))
+	 hyps tclIDTAC gls 
+
+(* tactics for consider/given *)
+
+let update_goal_info gls =
+  let info = get_its_info gls in
+    match info.pm_subgoals with
+	[m,_] -> tcl_change_info {info with pm_subgoals =[m,pf_concl gls]} gls
+      | _ -> error "thesis is split"
+
+let conjunction_arity id gls =
+  let typ = pf_get_hyp_typ gls id  in
+  let hd,params = decompose_app (special_whd gls typ) in
+  let env =pf_env gls in 
+    match kind_of_term hd with
+	Ind ind when is_good_inductive env ind ->
+	  let mib,oib=
+	    Inductive.lookup_mind_specif env ind in
+          let gentypes=
+            Inductive.arities_of_constructors ind (mib,oib) in
+	  let _ = if Array.length gentypes <> 1 then raise Not_found in
+	  let apptype = Term.prod_applist gentypes.(0) params in
+	  let rc,_ = Reduction.dest_prod env apptype in
+	    List.length rc
+      | _ -> raise Not_found
+
+let rec intron_then n ids ltac gls = 
+  if n<=0 then 
+    tclTHEN
+    (fun gls -> 
+       if List.exists (fun id -> occur_id [] id (pf_concl gls)) ids  then 
+	 update_goal_info gls
+       else 
+	 tclIDTAC gls)
+    (ltac ids)
+      gls
+  else  
+    let id = pf_get_new_id (id_of_string "_tmp") gls in 
+      tclTHEN 
+	(intro_mustbe_force id) 
+	(intron_then (pred n) (id::ids) ltac) gls 
+
+let pm_rename_hyp id hid gls =
+  if occur_id [] id (pf_concl gls) then
+    tclTHEN (rename_hyp id hid) update_goal_info gls
+  else
+    rename_hyp id hid gls 
+
+let rec consider_match may_intro introduced available expected gls =
+  match available,expected with 
+      [],[] ->
+	if not may_intro then 
+	  set_last (List.hd introduced) gls
+	else
+	  let info = get_its_info gls in 
+	  let nameset=List.fold_right Idset.add introduced info.pm_hyps in
+	    tcl_change_info {info with 
+			       pm_last = Name (List.hd introduced);
+			       pm_hyps = nameset} gls
+    | _,[] -> error "last statements do not match a complete hypothesis" 
+	(* should tell which ones *)
+    | [],hyps -> 
+	if may_intro then
+	  begin
+ 	    let id = pf_get_new_id (id_of_string "_tmp") gls in
+	      tclIFTHENELSE 
+		(intro_pm id)
+		(consider_match true [] [id] hyps) 
+		(fun _ -> 
+		   error "not enough sub-hypotheses to match statements")
+		gls 
+          end
+	else
+	  error "not enough sub-hypotheses to match statements" 
+	    (* should tell which ones *)
+    | id::rest_ids,(Hvar st | Hprop st)::rest ->
+	tclIFTHENELSE (convert_hyp (id,None,st.st_it))
+	  begin
+	    match st.st_label with 
+		Anonymous -> 
+		  consider_match may_intro (id::introduced) rest_ids rest
+	      | Name hid -> 
+		  tclTHENLIST 
+		    [pm_rename_hyp id hid;
+		     consider_match may_intro (hid::introduced) rest_ids rest]
+	  end
+	  begin
+	    (fun gls -> 
+	       let nhyps =
+		 try conjunction_arity id gls with 
+		     Not_found -> error "matching hypothesis not found" in 
+		 tclTHENLIST 
+		   [general_case_analysis (mkVar id,NoBindings);
+		    intron_then nhyps []
+		      (fun l -> consider_match may_intro introduced 
+			 (List.rev_append l rest_ids) expected)] gls)
+	  end
+	  gls
+	  
+let consider_tac c hyps gls =
+  match kind_of_term (strip_outer_cast c) with
+      Var id ->
+	consider_match false [] [id] hyps gls 
+    | _ -> 
+	let id = pf_get_new_id (id_of_string "_tmp") gls in
+	tclTHEN 
+	  (forward None (Genarg.IntroIdentifier id) c)
+ 	  (consider_match false [] [id] hyps) gls 
+	  
+
+let given_tac hyps gls =
+  consider_match true [] [] hyps gls
+
+(* tactics for take *)
+
+let rec take_tac wits gls =
+  match wits with
+      [] -> tclIDTAC gls
+    | wit::rest ->  
+	let typ = pf_type_of gls wit in  
+	  tclTHEN (thus_tac wit typ) (take_tac rest)  gls
+
+
+(* tactics for define *)
+
+let rec build_function args body =
+  match args with 
+      st::rest -> 
+	let pfun= lift 1 (build_function rest body) in
+	let id = match st.st_label with
+	    Anonymous -> assert false
+	  | Name id -> id in
+	  mkLambda (Name id, st.st_it, subst_term (mkVar id) pfun)
+    | [] -> body 
+
+let define_tac id args body gls =
+  let t = build_function args body in
+    letin_tac true (Name id) t Tacexpr.nowhere gls
+
+(* tactics for reconsider *)
+
+let cast_tac id_or_thesis typ gls = 
+  let info = get_its_info gls in
+  match id_or_thesis with
+      This id ->
+	let (_,body,_) = pf_get_hyp gls id in
+	  convert_hyp (id,body,typ) gls
+    | Thesis (For _ ) -> 
+	error "\"thesis for ...\" is not applicable here" 
+    | Thesis (Sub n) ->
+	begin
+	  let old_typ = 
+	    try List.assoc n info.pm_subgoals 
+	    with Not_found -> error "No such part in thesis." in
+	  if is_conv_leq (pf_env gls) (sig_sig gls) typ old_typ then
+	    let new_sg = List.merge  
+	      (fun (n,_) (p,_) -> Pervasives.compare n p) 
+	      [n,typ] (List.remove_assoc n info.pm_subgoals) in
+	      tcl_change_info {info with pm_subgoals=new_sg} gls
+	  else 
+	    error "not convertible"
+	end
+    | Thesis Plain ->   
+	match info.pm_subgoals with 
+	    [m,c] -> 
+	      tclTHEN 
+		(convert_concl typ DEFAULTcast) 
+	        (tcl_change_info {info with pm_subgoals= [m,typ]}) gls
+	  | _ -> error 
+	      "\"thesis\" is split, please specify which part you refer to."
+  
+      
+(* per cases *)
+
+let start_tree env ind = 
+  let constrs = (snd (Inductive.lookup_mind_specif env ind)).mind_consnames in
+    Split (Idset.empty,ind,Array.map (fun _ -> None) constrs)
+
+let build_per_info etype casee gls = 
+  let concl=get_thesis gls in
+  let env=pf_env gls in
+  let ctyp=pf_type_of gls casee in
+  let is_dep = dependent casee concl in 
+  let hd,args = decompose_app (special_whd gls ctyp) in
+  let ind = 
+    try
+      destInd hd 
+    with _ -> 
+      error "Case analysis must be done on an inductive object" in
+  let nparams =
+    let mind = fst (Global.lookup_inductive ind) in
+     match etype with
+	 ET_Induction -> mind.mind_nparams_rec
+       | _ -> mind.mind_nparams in
+  let params,real_args = list_chop nparams args in
+  let abstract_obj body c = 
+    let typ=pf_type_of gls c in 
+      lambda_create env (typ,subst_term c body) in
+  let pred= List.fold_left abstract_obj    
+    (lambda_create env (ctyp,subst_term casee concl)) real_args in
+    is_dep,
+  {per_casee=casee;
+   per_ctype=ctyp;
+   per_ind=ind;
+   per_pred=pred;
+   per_args=real_args;
+   per_params=params;
+   per_nparams=nparams}
+
+let per_tac etype casee gls=
+  let env=pf_env gls in
+  let info = get_its_info gls in
+    match casee with
+	Real c ->
+	  let is_dep,per_info = build_per_info etype c gls in
+	  let ek = 
+	    if is_dep then
+	      EK_dep (start_tree env per_info.per_ind)
+	    else EK_unknown in
+	    tcl_change_info 
+	      {info with 
+		 pm_stack=
+		  Per(etype,per_info,ek,[])::info.pm_stack} gls
+      | Virtual cut ->
+	  assert (cut.cut_stat.st_label=Anonymous);
+	  let id = pf_get_new_id (id_of_string "_matched") gls in
+	  let c = mkVar id in
+	  let modified_cut = 
+	    {cut with cut_stat={cut.cut_stat with st_label=Name id}} in
+	    tclTHEN 
+	      (instr_cut (fun _ c -> c) false false modified_cut)
+	      (fun gls0 ->
+		 let is_dep,per_info = build_per_info etype c gls0 in
+		   assert (not is_dep);
+		   tcl_change_info 
+		     {info with pm_stack=
+			 Per(etype,per_info,EK_unknown,[])::info.pm_stack} gls0)
+	      gls
+
+(* suppose *)
+
+let rec build_product args body =
+  match args with 
+      (Hprop st| Hvar st )::rest -> 
+	let pprod= lift 1 (build_product rest body) in
+	let lbody =
+	  match st.st_label with
+	      Anonymous -> body
+	    | Name id -> subst_term (mkVar id) pprod in
+	  mkProd (st.st_label, st.st_it, lbody)
+    | [] -> body 
+
+let register_nodep_subcase id= function
+    Per(et,pi,ek,clauses)::s ->
+      begin
+	match ek with
+	    EK_unknown -> clauses,Per(et,pi,EK_nodep,id::clauses)::s
+	  | EK_nodep -> clauses,Per(et,pi,EK_nodep,id::clauses)::s
+	  | EK_dep _ -> error "Do not mix \"suppose\" with \"suppose it is\"."
+      end
+  | _ -> anomaly "wrong stack state"
+
+let suppose_tac hyps gls0 = 
+  let info = get_its_info gls0 in
+  let thesis = get_thesis gls0 in
+  let id = pf_get_new_id (id_of_string "_subcase") gls0 in
+  let clause = build_product hyps thesis in
+  let ninfo1 = {info with 
+		  pm_stack=Suppose_case::info.pm_stack;
+		  pm_partial_goal=mkMeta 1;
+		  pm_subgoals = [1,clause]} in
+  let old_clauses,stack = register_nodep_subcase id info.pm_stack in
+  let ninfo2 = {info with 
+		  pm_stack=stack} in
+    tclTHENS (internal_cut id clause) 
+      [tclTHENLIST [tcl_change_info ninfo1;
+		    assume_tac hyps;
+		    clear old_clauses];
+       tcl_change_info ninfo2] gls0
+
+(* suppose it is ... *) 
+
+(* pattern matching compiling *)
+
+let rec nb_prod_after n c=
+  match kind_of_term c with
+    | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else 
+	1+(nb_prod_after 0 b)
+    | _ -> 0
+
+let constructor_arities env ind =
+  let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
+  let constr_types = Inductiveops.arities_of_constructors env ind in 
+  let hyp = nb_prod_after nparams in	
+    Array.map hyp constr_types
+
+let rec n_push rest ids n = 
+  if n<=0 then Pop rest else Push (ids,n_push rest ids (pred n)) 
+
+let explode_branches ids env ind rest=
+  Array.map (fun n -> Some (Idset.empty,n_push rest ids n)) (constructor_arities env ind)
+
+let rec tree_of_pats env ((id,_) as cpl) pats =
+  match pats with 
+      [] -> End_of_branch cpl
+    | args::stack ->
+	match args with
+	    [] -> Pop (tree_of_pats env cpl stack)
+	  | patt :: rest_args ->
+	      match patt with
+		  PatVar (_,v) -> 
+		    Push (Idset.singleton id,
+			  tree_of_pats env cpl (rest_args::stack))
+		|  PatCstr (_,(ind,cnum),args,nam) ->
+		     let _,mind = Inductive.lookup_mind_specif env ind in
+		     let br= Array.map (fun _ -> None) mind.mind_consnames in
+		       br.(pred cnum) <- 
+			 Some (Idset.singleton id,
+			       tree_of_pats env cpl (args::rest_args::stack));
+		       Split(Idset.empty,ind,br)
+
+let rec add_branch env ((id,_) as cpl) pats tree=
+  match pats with 
+      [] -> 
+	begin
+	  match tree with
+	      End_of_branch cpl0 -> End_of_branch cpl0 
+		(* this ensures precedence *) 
+	    | _ -> anomaly "tree is expected to end here"
+	end
+    | args::stack ->
+	match args with 
+	    [] ->
+	      begin
+		match tree with 
+		    Pop t -> Pop (add_branch env cpl stack t)
+		  | _ -> anomaly "we should pop here" 
+	      end
+	  | patt :: rest_args ->
+	      match patt with
+		  PatVar (_,v) ->
+		    begin
+		      match tree with 
+			  Push (ids,t) -> 
+			    Push (Idset.add id ids,
+				  add_branch env cpl (rest_args::stack) t)
+			| Split (ids,ind,br) ->
+			    Split (Idset.add id ids,
+				   ind,array_map2 
+				     (append_branch env cpl 1 
+					(rest_args::stack)) 
+				     (constructor_arities env ind) br)
+			| _ -> anomaly "No pop/stop expected here"  
+		    end
+		| PatCstr (_,(ind,cnum),args,nam) ->
+		    match tree with
+			Push (ids,t) ->
+			  let br = explode_branches ids env ind t in
+			  let _ =
+			    br.(pred cnum)<- 
+			      option_map
+			      (fun (ids,tree) -> 
+				 Idset.add id ids,
+				 add_branch env cpl 
+				   (args::rest_args::stack) tree) 
+			      br.(pred cnum) in
+			    Split (ids,ind,br)
+		      | Split (ids,ind0,br0) ->
+			  if (ind <> ind0) then error
+			    (* this can happen with coercions *)
+	                      "Case pattern belongs to wrong inductive type";
+			  let br=Array.copy br0 in
+			  let ca = constructor_arities env ind in
+			  let _= br.(pred cnum)<-
+			    append_branch env cpl 0 (args::rest_args::stack) 
+			    ca.(pred cnum) br.(pred cnum) in 
+			    Split (ids,ind,br)
+		      | _ -> anomaly "No pop/stop expected here"
+and append_branch env ((id,_) as cpl) depth pats nargs = function
+    Some (ids,tree) -> 
+      Some (Idset.add id ids,append_tree env cpl depth pats tree)
+  | None ->
+      Some (* (n_push (tree_of_pats env cpl pats) 
+	      (Idset.singleton id) nargs) *)
+	   (Idset.singleton id,tree_of_pats env cpl pats)
+and append_tree env ((id,_) as cpl) depth pats tree =
+  if depth<=0 then add_branch env cpl pats tree
+  else match tree with
+      Pop t -> Pop (append_tree env cpl (pred depth) pats t)
+    | Push (ids,t) -> Push (Idset.add id ids,
+				   append_tree env cpl depth pats t)
+    | End_of_branch _ -> anomaly "Premature end of branch"
+    | Split (ids,ind,branches) -> 
+	Split (Idset.add id ids,ind,
+	       array_map2 
+		 (append_branch env cpl (succ depth) pats) 
+		 (constructor_arities env ind)
+		 branches)
+
+(* suppose it is *)
+
+let rec st_assoc id = function
+    [] -> raise Not_found
+  | st::_ when st.st_label = id  -> st.st_it
+  | _ :: rest -> st_assoc id rest
+
+let thesis_for obj typ per_info env=
+  let rc,hd1=decompose_prod typ in
+  let cind,all_args=decompose_app typ in
+  let ind = destInd cind in
+  let _ = if ind <> per_info.per_ind then
+    errorlabstrm "thesis_for" 
+      ((Printer.pr_constr_env env obj) ++ spc () ++ 
+	 str "cannot give an induction hypothesis (wrong inductive type)") in  
+  let params,args = list_chop per_info.per_nparams all_args in
+  let _ = if not (List.for_all2 eq_constr params per_info.per_params) then
+    errorlabstrm "thesis_for" 
+      ((Printer.pr_constr_env env obj) ++ spc () ++ 
+	 str "cannot give an induction hypothesis (wrong parameters)") in
+  let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in
+    compose_prod rc (whd_beta hd2)
+
+let rec build_product_dep pat_info per_info args body gls =
+  match args with 
+      (Hprop {st_label=nam;st_it=This c} 
+      | Hvar {st_label=nam;st_it=c})::rest -> 
+	let pprod= 
+	  lift 1 (build_product_dep pat_info per_info rest body gls) in
+	let lbody =
+	  match nam with
+	      Anonymous -> body
+	    | Name id -> subst_var id pprod in
+	  mkProd (nam,c,lbody)
+    | Hprop ({st_it=Thesis tk} as st)::rest ->
+	let pprod= 
+	  lift 1 (build_product_dep pat_info per_info rest body gls) in
+	let lbody =
+	  match st.st_label with
+	      Anonymous -> body
+	    | Name id -> subst_var id pprod in
+	let ptyp =
+	  match tk with
+	      For id ->
+		let obj = mkVar id in
+		let typ = 
+		  try st_assoc (Name id) pat_info.pat_vars 
+		  with Not_found -> 
+		    snd (st_assoc (Name id) pat_info.pat_aliases) in
+		  thesis_for obj typ per_info (pf_env gls)
+	    | Plain -> get_thesis gls 
+	    | Sub n -> anomaly "Subthesis in cases" in
+	  mkProd (st.st_label,ptyp,lbody)
+    | [] -> body 
+
+let build_dep_clause params pat_info per_info hyps gls =
+  let concl=
+    thesis_for pat_info.pat_constr pat_info.pat_typ per_info (pf_env gls) in
+  let open_clause =
+    build_product_dep pat_info per_info hyps concl gls in
+  let prod_one st body =
+    match st.st_label with
+	Anonymous -> mkProd(Anonymous,st.st_it,lift 1 body)
+      | Name id -> mkNamedProd id st.st_it (lift 1 body) in
+  let let_one_in st body =
+    match st.st_label with
+	Anonymous -> mkLetIn(Anonymous,fst st.st_it,snd st.st_it,lift 1 body)
+      | Name id -> 
+	  mkNamedLetIn id (fst st.st_it) (snd st.st_it) (lift 1 body) in
+  let aliased_clause = 
+    List.fold_right let_one_in pat_info.pat_aliases open_clause in
+    List.fold_right prod_one (params@pat_info.pat_vars) aliased_clause
+
+let rec register_dep_subcase id env per_info pat = function
+    EK_nodep -> error  "Only \"suppose it is\" can be used here."
+  | EK_unknown -> 
+      register_dep_subcase id env per_info pat
+	(EK_dep (start_tree env per_info.per_ind))
+  | EK_dep tree -> EK_dep (add_branch env id [[pat]] tree)
+  
+let case_tac params pat_info hyps gls0 =
+  let info = get_its_info gls0 in
+  let id = pf_get_new_id (id_of_string "_subcase") gls0 in
+  let et,per_info,ek,old_clauses,rest =
+    match info.pm_stack with
+	Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest) 
+      | _ -> anomaly "wrong place for cases" in
+  let clause = build_dep_clause params pat_info per_info hyps gls0 in
+  let ninfo1 = {info with 
+		  pm_stack=Suppose_case::info.pm_stack;
+		  pm_partial_goal=mkMeta 1;
+		  pm_subgoals = [1,clause]} in
+  let nek = 
+    register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info 
+      pat_info.pat_pat ek in  
+  let ninfo2 = {info with 
+		  pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in
+    tclTHENS (internal_cut id clause) 
+      [tclTHENLIST 
+	 [tcl_change_info ninfo1; 
+	  assume_st (params@pat_info.pat_vars);
+	  assume_st_letin pat_info.pat_aliases;
+	  assume_hyps_or_theses hyps;
+	  clear old_clauses];
+       tcl_change_info ninfo2] gls0
+
+(* end cases *)
+
+type instance_stack =
+    (constr option*bool*(constr list) list) list
+
+let initial_instance_stack ids =
+  List.map (fun id -> id,[None,false,[]]) ids
+
+let push_one_arg arg = function 
+    [] -> anomaly "impossible"
+  | (head,is_rec,args) :: ctx -> 
+      ((head,is_rec,(arg::args)) :: ctx)
+
+let push_arg arg stacks =
+  List.map (fun (id,stack) -> (id,push_one_arg arg stack)) stacks
+  
+
+let push_one_head c is_rec ids (id,stack) = 
+  let head = if Idset.mem id ids then Some c else None in
+    id,(head,is_rec,[]) :: stack
+
+let push_head c is_rec ids stacks =
+  List.map (push_one_head c is_rec ids) stacks
+
+let pop_one rec_flag (id,stack) =  
+  let nstack=
+    match stack with
+	[] -> anomaly "impossible"
+      | [c] as l -> l
+      | (Some head,is_rec,args)::(head0,is_rec0,args0)::ctx ->
+	  let arg = applist (head,(List.rev args)) in
+	    rec_flag:= !rec_flag || is_rec;
+	    (head0,is_rec0,(arg::args0))::ctx
+     | (None,is_rec,args)::(head0,is_rec0,args0)::ctx ->
+	 rec_flag:= !rec_flag || is_rec;
+	 (head0,is_rec0,(args@args0))::ctx
+  in id,nstack
+
+let pop_stacks stacks =
+  let rec_flag= ref false in 
+  let nstacks = List.map (pop_one rec_flag) stacks in
+    !rec_flag , nstacks
+
+let patvar_base = id_of_string "__"
+
+let test_fun (str:string) = ()
+
+let hrec_for obj_id fix_id per_info gls=
+  let obj=mkVar obj_id in
+  let typ=pf_get_hyp_typ gls obj_id in
+  let rc,hd1=decompose_prod typ in
+  let cind,all_args=decompose_app typ in
+    match kind_of_term cind with
+	Ind ind when ind=per_info.per_ind ->
+	  let params,args= list_chop per_info.per_nparams all_args in 
+	    if try 
+	      (List.for_all2 eq_constr params per_info.per_params)
+	    with Invalid_argument _ -> false then
+	      let hd2 = applist (mkVar fix_id,args@[obj]) in
+		Some (compose_lam rc (whd_beta hd2))
+	    else None
+      | _ -> None
+
+let rec execute_cases at_top fix_name per_info kont0 stacks tree gls = 
+  match tree with
+      Pop t ->  
+	let is_rec,nstacks =  pop_stacks stacks in
+	  if is_rec then
+	    let _ = test_fun "is_rec=true" in
+	     let c_id = pf_get_new_id (id_of_string "_hrec") gls in
+	       tclTHEN 
+		 (intro_mustbe_force c_id)
+		 (execute_cases false fix_name per_info kont0 nstacks t) gls
+	  else
+	    execute_cases false fix_name per_info kont0 nstacks t gls
+    | Push (_,t) -> 
+	let id = pf_get_new_id patvar_base gls in
+	let nstacks = push_arg (mkVar id) stacks in
+	let kont = execute_cases false fix_name per_info kont0 nstacks t in
+	  tclTHEN
+	    (intro_mustbe_force id)
+	    begin
+	      match fix_name with
+		  Anonymous -> kont
+		| Name fix_id ->  
+		    (fun gls -> 
+		       if at_top then
+			 kont gls
+		       else
+			 match hrec_for id fix_id per_info gls with
+			     None -> kont gls
+			   | Some c_obj ->
+			       let c_id = 
+				 pf_get_new_id (id_of_string "_hrec") gls in
+				 tclTHENLIST 
+				   [generalize [c_obj];
+				    intro_mustbe_force c_id;
+				    kont] gls)
+	    end gls
+    | Split(ids,ind,br) ->
+	let (_,typ,_)=destProd (pf_concl gls) in
+	let hd,args=decompose_app (special_whd gls typ) in
+	let _ = assert (ind = destInd hd) in
+	let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
+	let params = list_firstn nparams args in
+	let constr i =applist (mkConstruct(ind,succ i),params) in
+	let next_tac is_rec i = function
+	    Some (sub_ids,tree) ->
+	      let br_stacks =
+		List.filter (fun (id,_) -> Idset.mem id sub_ids) stacks in
+	      let p_stacks = 
+		push_head (constr i) is_rec ids br_stacks in
+		execute_cases false fix_name per_info kont0 p_stacks tree 
+	  | None -> 
+	      msgnl (str "Warning : missing case");
+	      kont0 (mkMeta 1) 
+	in
+	let id = pf_get_new_id patvar_base gls in
+	let kont is_rec = 			
+	  tclTHENSV
+	    (general_case_analysis (mkVar id,NoBindings))
+	    (Array.mapi (next_tac is_rec) br) in
+	  tclTHEN 
+	    (intro_mustbe_force id)
+	    begin
+	      match fix_name with
+		  Anonymous -> kont false
+		| Name fix_id ->  
+		    (fun gls -> 
+		       if at_top then
+			 kont false gls
+		       else
+			 match hrec_for id fix_id per_info gls with
+			     None -> kont false gls
+			   | Some c_obj ->
+			       tclTHENLIST 
+				 [generalize [c_obj];
+				  kont true] gls)
+	    end gls
+    | End_of_branch (id,nhyps) -> 
+	  match List.assoc id stacks with
+	      [None,_,args] -> 
+		let metas = list_tabulate (fun n -> mkMeta (succ n)) nhyps in
+		  kont0 (applist (mkVar id,List.rev_append args metas)) gls
+	    | _ -> anomaly "wrong stack size"
+
+let end_tac et2 gls =
+  let info = get_its_info gls in
+  let et1,pi,ek,clauses = 
+    match info.pm_stack with
+	Suppose_case::_ -> 
+	  anomaly "This case should already be trapped"
+      | Claim::_ ->  
+	  error "\"end claim\" expected."
+      | Focus_claim::_ ->
+	  error "\"end focus\" expected."
+      | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses) 
+      | [] -> 
+	  anomaly "This case should already be trapped" in
+  let et = 
+    if et1 <> et2 then
+      match et1 with 
+	  ET_Case_analysis -> 
+	    error "\"end cases\" expected."
+	| ET_Induction ->
+	    error "\"end induction\" expected."
+    else et1 in
+    tclTHEN 
+      tcl_erase_info
+      begin
+	match et,ek with
+	    _,EK_unknown -> 
+	      tclSOLVE [simplest_elim pi.per_casee]	
+	  | ET_Case_analysis,EK_nodep ->
+	      tclTHEN 
+		(general_case_analysis (pi.per_casee,NoBindings))
+		(default_justification (List.map mkVar clauses))
+	  | ET_Induction,EK_nodep ->
+	      tclTHENLIST
+		[generalize (pi.per_args@[pi.per_casee]); 
+		 simple_induct (AnonHyp (succ (List.length pi.per_args)));
+		 default_justification (List.map mkVar clauses)]
+	  | ET_Case_analysis,EK_dep tree ->
+	      tclTHENLIST 
+		[generalize (pi.per_args@[pi.per_casee]);
+		 execute_cases true Anonymous pi 
+		   (fun c -> tclTHENLIST 
+		      [refine c;
+		       clear clauses;
+		       justification assumption])
+		   (initial_instance_stack clauses) tree]	
+	  | ET_Induction,EK_dep tree ->
+	      tclTHEN (generalize (pi.per_args@[pi.per_casee]))
+		begin
+		  fun gls0 -> 
+		    let fix_id = pf_get_new_id (id_of_string "_fix") gls0 in
+		      tclTHEN 
+			(fix (Some fix_id) (succ (List.length pi.per_args))) 
+			(execute_cases true (Name fix_id) pi 
+			   (fun c ->
+			      tclTHENLIST 
+				[clear [fix_id];
+				 refine c;
+				 clear clauses;
+				 justification assumption
+				 (* justification automation_tac *)])
+			   (initial_instance_stack clauses) tree) gls0
+		end	
+      end gls
+
+(* escape *)
+
+let rec abstract_metas n avoid head = function
+    [] -> 1,head,[]
+  | (meta,typ)::rest -> 
+      let id = Nameops.next_ident_away (id_of_string "_sbgl") avoid in
+      let p,term,args = abstract_metas (succ n) (id::avoid) head rest in 
+	succ p,mkLambda(Name id,typ,subst_meta [meta,mkRel p] term),
+      (mkMeta n)::args 
+
+let build_refining_context gls =
+  let info = get_its_info gls in
+  let avoid=pf_ids_of_hyps gls in
+  let _,fn,args=abstract_metas 1 avoid info.pm_partial_goal info.pm_subgoals in
+    applist (fn,args)
+    
+let escape_command pts =
+  let pts1 = nth_unproven 1 pts in
+  let gls = top_goal_of_pftreestate pts1 in
+  let term = build_refining_context gls in
+  let tac = tclTHEN 
+    (abstract_operation (Proof_instr (true,{emph=0;instr=Pescape})) tcl_erase_info)
+    (Tactics.refine term) in
+    traverse 1 (solve_pftreestate tac pts1)
+
+(* General instruction engine *)
+
+let rec do_proof_instr_gen _thus _then instr = 
+  match instr with 
+      Pthus i -> 
+	assert (not _thus);
+	do_proof_instr_gen true _then i
+    | Pthen i -> 	
+	assert (not _then);
+	do_proof_instr_gen _thus true i
+    | Phence i -> 
+	assert (not (_then || _thus));
+	do_proof_instr_gen true true i
+    | Pcut c ->
+	instr_cut mk_stat_or_thesis _thus _then c
+    | Prew (s,c) ->
+	assert (not _then);
+	instr_rew _thus s c
+    | Pconsider (c,hyps)    -> consider_tac c hyps
+    | Pgiven hyps            -> given_tac hyps
+    | Passume hyps           -> assume_tac hyps
+    | Plet hyps              -> assume_tac hyps
+    | Pclaim st              -> instr_claim false st 
+    | Pfocus st              -> instr_claim true st
+    | Ptake witl             -> take_tac witl
+    | Pdefine (id,args,body) -> define_tac id args body
+    | Pcast (id,typ)         -> cast_tac id typ 
+    | Pper (et,cs)           -> per_tac et cs 
+    | Psuppose hyps      -> suppose_tac hyps
+    | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps
+    | Pend (B_elim et) -> end_tac et
+    | Pend _ | Pescape -> anomaly "Not applicable"
+ 
+let eval_instr {instr=instr} =
+  do_proof_instr_gen false false instr   
+
+let rec preprocess pts instr =
+  match instr with
+    Phence i |Pthus i | Pthen i -> preprocess pts i
+  | Pcut _ |  Passume _ | Plet _ | Pclaim _ | Pfocus _ 
+  | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _ 
+  | Pdefine (_,_,_) | Pper _ | Prew _ ->
+      check_not_per pts;
+      true,pts
+  | Pescape -> 
+      check_not_per pts;
+      false,pts
+  | Pcase _ | Psuppose _ | Pend (B_elim _) -> 
+      true,close_previous_case pts
+  | Pend bt -> 
+      false,close_block bt pts 
+      
+let rec postprocess pts instr = 
+  match instr with
+      Phence i | Pthus i | Pthen i -> postprocess pts i
+    | Pcut _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_)
+    | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> pts
+    | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ -> nth_unproven 1 pts
+    | Pescape ->
+	escape_command pts
+    | Pend _ -> 
+	goto_current_focus_or_top (mark_as_done pts)
+
+let do_instr raw_instr pts =
+  let has_tactic,pts1 = preprocess pts raw_instr.instr in
+  let pts2 = 
+    if has_tactic then
+      let gl = nth_goal_of_pftreestate 1 pts1 in
+      let env=  pf_env gl in
+      let sigma= project gl in
+      let ist = {ltacvars = ([],[]); ltacrecvars = []; 
+		 gsigma = sigma; genv = env} in
+      let glob_instr = intern_proof_instr ist raw_instr in
+      let instr = 
+	interp_proof_instr (get_its_info gl) sigma env glob_instr in
+      let lock_focus = is_focussing_instr instr.instr in
+      let marker= Proof_instr (lock_focus,instr) in
+	solve_nth_pftreestate 1 
+	  (abstract_operation marker (eval_instr instr)) pts1
+    else pts1 in
+      postprocess pts2 raw_instr.instr
+
+let proof_instr raw_instr =
+  Pfedit.mutate (do_instr raw_instr)
+
+(*
+
+(* STUFF FOR ITERATED RELATIONS *)
+let decompose_bin_app t= 
+  let hd,args = destApp 
+
+let identify_transitivity_lemma c =
+  let varx,tx,c1 = destProd c in
+  let vary,ty,c2 = destProd (pop c1) in
+  let varz,tz,c3 = destProd (pop c2) in
+  let _,p1,c4 = destProd (pop c3) in
+  let _,lp2,lp3 = destProd (pop c4) in
+  let p2=pop lp2 in
+  let p3=pop lp3 in
+*)
+    
diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli
new file mode 100644
index 00000000..ba8dc7b6
--- /dev/null
+++ b/tactics/decl_proof_instr.mli
@@ -0,0 +1,118 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Refiner
+open Names
+open Term
+open Tacmach
+
+val go_to_proof_mode: unit -> unit
+val return_from_tactic_mode: unit -> unit
+
+val register_automation_tac: tactic -> unit
+
+val automation_tac : tactic
+
+val daimon_subtree: pftreestate -> pftreestate
+
+val do_instr: Decl_expr.raw_proof_instr -> pftreestate -> pftreestate
+val proof_instr: Decl_expr.raw_proof_instr -> unit
+
+val tcl_change_info : Decl_mode.pm_info -> tactic
+
+val mark_proof_tree_as_done : Proof_type.proof_tree -> Proof_type.proof_tree
+
+val mark_as_done : pftreestate -> pftreestate
+
+val execute_cases : bool ->
+    Names.name ->
+    Decl_mode.per_info ->
+    (Term.constr -> Proof_type.tactic) ->
+    (Names.Idset.elt * (Term.constr option * bool * Term.constr list) list) 
+      list ->
+    Decl_mode.split_tree -> Proof_type.tactic
+
+val tree_of_pats :
+    Environ.env ->
+    Names.Idset.elt * int ->
+    Rawterm.cases_pattern list list -> Decl_mode.split_tree
+val add_branch :
+    Environ.env ->
+    Names.Idset.elt * int ->
+    Rawterm.cases_pattern list list ->
+    Decl_mode.split_tree -> Decl_mode.split_tree
+val append_branch :
+    Environ.env ->
+    Names.Idset.elt * int ->
+    int ->
+    Rawterm.cases_pattern list list ->
+    int ->
+    (Names.Idset.t * Decl_mode.split_tree) option ->
+    (Names.Idset.t * Decl_mode.split_tree) option
+
+val append_tree :   Environ.env ->
+    Names.Idset.elt * int ->
+    int ->
+    Rawterm.cases_pattern list list ->
+    Decl_mode.split_tree -> Decl_mode.split_tree
+
+val build_dep_clause :   Term.types Decl_expr.statement list ->
+    Decl_expr.proof_pattern ->
+    Decl_mode.per_info ->
+    (Term.types Decl_expr.statement, Term.types Decl_expr.or_thesis)
+    Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types
+
+val register_dep_subcase :    
+    Names.identifier * int ->
+    Environ.env ->
+    Decl_mode.per_info ->
+    Rawterm.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind
+
+val thesis_for :     Term.constr ->
+    Term.constr -> Decl_mode.per_info -> Environ.env -> Term.constr
+
+val close_previous_case : pftreestate -> pftreestate
+
+val test_fun : string -> unit
+
+
+val pop_stacks :
+  (Names.identifier * 
+     (Term.constr option * bool * Term.constr list) list) list ->
+  bool * 
+    (Names.identifier * 
+       (Term.constr option * bool * Term.constr list) list) list
+
+
+val push_head :   Term.constr ->
+  bool ->
+  Names.Idset.t ->
+  (Names.identifier * 
+     (Term.constr option * bool * Term.constr list) list) list ->
+  (Names.identifier * 
+     (Term.constr option * bool * Term.constr list) list) list
+
+val push_arg : Term.constr ->
+  (Names.identifier * 
+     (Term.constr option * bool * Term.constr list) list) list ->
+  (Names.identifier * 
+     (Term.constr option * bool * Term.constr list) list) list
+
+val hrec_for: 
+    Names.identifier ->
+    Names.identifier ->
+    Decl_mode.per_info -> Proof_type.goal Tacmach.sigma -> Term.constr option
+
+val consider_match :
+   bool ->
+    Names.Idset.elt list ->
+    Names.Idset.elt list ->
+    (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list ->
+    Proof_type.tactic
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 32abc347..6da0dd49 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: eauto.ml4 8878 2006-05-30 16:44:25Z herbelin $ *)
+(* $Id: eauto.ml4 9277 2006-10-25 13:02:22Z herbelin $ *)
 
 open Pp
 open Util
@@ -46,7 +46,7 @@ END
 
 let e_resolve_with_bindings_tac  (c,lbind) gl = 
   let t = pf_hnf_constr gl (pf_type_of gl c) in 
-  let clause = make_clenv_binding_apply gl (-1) (c,t) lbind in 
+  let clause = make_clenv_binding_apply gl None (c,t) lbind in 
   Clenvtac.e_res_pf clause gl
 
 let e_resolve_constr c gls = e_resolve_with_bindings_tac (c,NoBindings) gls
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f05c3882..2526c84e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: equality.ml 9010 2006-07-05 07:17:41Z jforest $ *)
+(* $Id: equality.ml 9211 2006-10-05 12:38:33Z letouzey $ *)
 
 open Pp
 open Util
@@ -82,34 +82,34 @@ let elimination_sort_of_clause = function
 *)
 
 let general_rewrite_bindings_clause cls lft2rgt (c,l) gl =
-  let ctype = pf_type_of gl c in 
+  let ctype = pf_apply get_type_of gl c in 
   (* 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
+    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)
@@ -119,36 +119,39 @@ 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)
-
+    error "The \"at\" syntax isn't available yet for the rewrite/replace tactic"
+  else match cl.onhyps with 
+    | Some l -> 
+	(* If a precise list of locations is given, success is mandatory for
+	   each of these locations. *)
+	let rec do_hyps = function 
+	  | [] -> tclIDTAC
+	  | ((_,id),_) :: l -> 
+	      tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l)
+	in 
+	if not cl.onconcl then do_hyps l 
+	else tclTHENFIRST (general_rewrite_bindings l2r c) (do_hyps l)
+    | None -> 
+	(* Otherwise, if we are told to rewrite in all hypothesis via the 
+           syntax "* |-", we fail iff all the different rewrites fail *) 
+	let rec do_hyps_atleastonce = function 
+	  | [] -> (fun gl -> error "Nothing to rewrite.")
+	  | id :: l -> 
+	      tclIFTHENTRYELSEMUST 
+		(general_rewrite_bindings_in l2r id c) 
+		(do_hyps_atleastonce l)
+	in 
+	let do_hyps gl = 
+	  (* If the term to rewrite is an hypothesis, don't rewrite in itself *)
+	  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 do_hyps_atleastonce ids gl
+	in 
+	if not cl.onconcl then do_hyps 
+	else tclIFTHENTRYELSEMUST (general_rewrite_bindings l2r c) do_hyps
 
 (* Conditional rewriting, the success of a rewriting is related 
    to the resolution of the conditions by a given tactic *)
@@ -182,9 +185,14 @@ let rewriteRL_clause = function
    tac : Used to prove the equality c1 = c2 
    gl : goal *)
 
-let abstract_replace clause c2 c1 unsafe tac gl =
-  let t1 = pf_type_of gl c1 
-  and t2 = pf_type_of gl c2 in
+let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl = 
+  let try_prove_eq = 
+    match try_prove_eq_opt with 
+      | None -> tclIDTAC
+      | Some tac ->  tclTRY (tclCOMPLETE tac)
+  in
+  let t1 = pf_apply get_type_of gl c1 
+  and t2 = pf_apply get_type_of gl c2 in
   if unsafe or (pf_conv_x gl t1 t2) then
     let e = build_coq_eq () in
     let sym = build_coq_sym_eq () in
@@ -192,34 +200,28 @@ let abstract_replace clause c2 c1 unsafe tac gl =
     tclTHENS (assert_tac false Anonymous eq)
       [onLastHyp (fun id -> 
 	tclTHEN 
-	  (tclTRY (rewriteRL_clause clause (mkVar id,NoBindings)))
+	  (tclTRY (general_multi_rewrite false (mkVar id,NoBindings) clause))
 	  (clear [id]));
        tclFIRST
 	 [assumption;
 	  tclTHEN (apply sym) assumption;
-	  tclTRY (tclCOMPLETE tac)
+	  try_prove_eq
 	 ]
       ] gl
   else
     error "terms do not have convertible types"
+  
 
+let replace c2 c1 gl = multi_replace onConcl c2 c1 false None gl
 
-let replace c2 c1 gl = abstract_replace None c2 c1 false tclIDTAC gl
-
-let replace_in id c2 c1 gl = abstract_replace (Some id) c2 c1 false tclIDTAC gl
+let replace_in id c2 c1 gl = multi_replace (onHyp id) c2 c1 false None gl
 
-let replace_by c2 c1 tac gl = abstract_replace None c2 c1 false tac gl
+let replace_by c2 c1 tac gl = multi_replace onConcl c2 c1 false (Some tac) gl
 
-let replace_in_by id c2 c1 tac gl = abstract_replace (Some id) c2 c1 false tac gl
+let replace_in_by id c2 c1 tac gl = multi_replace (onHyp id) c2 c1 false (Some tac) gl
 
-
-let new_replace c2 c1 id tac_opt gl = 
-  let tac = 
-    match tac_opt with 
-      | Some tac -> tac 
-      | _ -> tclIDTAC
-  in
-  abstract_replace id c2 c1 false tac gl
+let replace_in_clause_maybe_by c2 c1 cl tac_opt gl = 
+  multi_replace cl c2 c1 false tac_opt gl
 
 (* End of Eduardo's code. The rest of this file could be improved
    using the functions match_with_equation, etc that I defined
@@ -269,24 +271,27 @@ exception DiscrFound of
   (constructor * int) list * constructor * constructor
 
 let find_positions env sigma t1 t2 =
-  let rec findrec posn t1 t2 =
+  let rec findrec sorts posn t1 t2 =
     let hd1,args1 = whd_betadeltaiota_stack env sigma t1 in
     let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in
     match (kind_of_term hd1, kind_of_term hd2) with
   	
       | Construct sp1, Construct sp2 
           when List.length args1 = mis_constructor_nargs_env env sp1
-          ->
-        (* both sides are fully applied constructors, so either we descend,
-           or we can discriminate here. *)
+            ->
+	  let sorts = list_intersect sorts (allowed_sorts env (fst sp1)) in
+          (* both sides are fully applied constructors, so either we descend,
+             or we can discriminate here. *)
 	  if sp1 = sp2 then
+	    let nrealargs = constructor_nrealargs env sp1 in
+	    let rargs1 = list_lastn nrealargs args1 in
+	    let rargs2 = list_lastn nrealargs args2 in
             List.flatten
-	      (list_map2_i
-		 (fun i arg1 arg2 ->
-		    findrec ((sp1,i)::posn) arg1 arg2)
-		 0 args1 args2)
-	  else
-	    raise (DiscrFound(List.rev posn,sp1,sp2))
+	      (list_map2_i (fun i -> findrec sorts ((sp1,i)::posn))
+		0 rargs1 rargs2)
+	  else if List.mem InType sorts then (* see build_discriminator *)
+	    raise (DiscrFound (List.rev posn,sp1,sp2))
+	  else []
 
       | _ ->
 	  let t1_0 = applist (hd1,args1) 
@@ -295,14 +300,13 @@ let find_positions env sigma t1 t2 =
 	    []
           else
 	    let ty1_0 = get_type_of env sigma t1_0 in
-	    match get_sort_family_of env sigma ty1_0 with
-	      | InSet | InType -> [(List.rev posn,t1_0,t2_0)]
-	      | InProp -> []
-	  in 
-	  (try 
-	     Inr(findrec [] t1 t2)
-	   with DiscrFound (path,c1,c2) -> 
-	     Inl (path,c1,c2))
+	    let s = get_sort_family_of env sigma ty1_0 in
+	    if List.mem s sorts then [(List.rev posn,t1_0,t2_0)] else [] in 
+  try
+    (* Rem: to allow injection on proofs objects, just add InProp *)
+    Inr (findrec [InSet;InType] [] t1 t2)
+  with DiscrFound (path,c1,c2) ->
+    Inl (path,c1,c2)
 
 let discriminable env sigma t1 t2 =
   match find_positions env sigma t1 t2 with
@@ -371,6 +375,7 @@ let discriminable env sigma t1 t2 =
 
    the continuation then constructs the case-split.
  *)
+
 let descend_then sigma env head dirn =
   let IndType (indf,_) =
     try find_rectype env sigma (get_type_of env sigma head)
@@ -383,9 +388,7 @@ let descend_then sigma env head dirn =
   (dirn_nlams,
    dirn_env,
    (fun dirnval (dfltval,resty) ->
-      let arsign,_ = get_arity env indf in
-      let depind = build_dependent_inductive env indf in
-      let deparsign = (Anonymous,None,depind)::arsign in
+      let deparsign = make_arity_signature env true indf in
       let p =
 	it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
       let build_branch i =
@@ -416,7 +419,7 @@ let descend_then sigma env head dirn =
 
 let construct_discriminator sigma env dirn c sort =
   let IndType(indf,_) =
-    try find_rectype env sigma (type_of env sigma c)
+    try find_rectype env sigma (get_type_of env sigma c)
     with Not_found ->
        (* one can find Rel(k) in case of dependent constructors 
           like T := c : (A:Set)A->T and a discrimination 
@@ -428,10 +431,8 @@ let construct_discriminator sigma env dirn c sort =
 		 dependent types") in
   let (ind,_) = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
-  let arsign,arsort = get_arity env indf in
   let (true_0,false_0,sort_0) = build_coq_True(),build_coq_False(),Prop Null in
-  let depind = build_dependent_inductive env indf in
-  let deparsign = (Anonymous,None,depind)::arsign in
+  let deparsign = make_arity_signature env true indf in
   let p = it_mkLambda_or_LetIn (mkSort sort_0) deparsign in
   let cstrs = get_constructors env indf in
   let build_branch i =
@@ -445,17 +446,22 @@ let construct_discriminator sigma env dirn c sort =
 let rec build_discriminator sigma env dirn c sort = function
   | [] -> construct_discriminator sigma env dirn c sort
   | ((sp,cnum),argnum)::l ->
-      let cty = type_of env sigma c in
-      let IndType (indf,_) =
-	try find_rectype env sigma cty with Not_found -> assert false in
-      let (ind,_) = dest_ind_family indf in
-      let (mib,mip) = lookup_mind_specif env ind in
-      let nparams = mib.mind_nparams  in
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
-      let newc = mkRel(cnum_nlams-(argnum-nparams)) in
+      let newc = mkRel(cnum_nlams-argnum) in
       let subval = build_discriminator sigma cnum_env dirn newc sort l  in
       kont subval (build_coq_False (),mkSort (Prop Null))
 
+(* Note: discrimination could be more clever: if some elimination is
+   not allowed because of a large impredicative constructor in the
+   path (see allowed_sorts in find_positions), the positions could
+   still be discrimated by projecting first instead of putting the
+   discrimination combinator inside the projecting combinator. Example
+   of relevant situation:
+
+   Inductive t:Set := c : forall A:Set, A -> nat -> t.
+   Goal ~ c _ 0 0 = c _ 0 1. intro. discriminate H.
+*)
+
 let gen_absurdity id gl =
   if is_empty_type (clause_type (onHyp id) gl)
   then
@@ -466,12 +472,12 @@ let gen_absurdity id gl =
 
 (* Precondition: eq is leibniz equality
  
-  returns ((eq_elim t t1 P i t2), absurd_term)
-  where  P=[e:t]discriminator 
-         absurd_term=False
+   returns ((eq_elim t t1 P i t2), absurd_term)
+   where  P=[e:t]discriminator 
+          absurd_term=False
 *)
 
-let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
+let discrimination_pf e (t,t1,t2) discriminator lbeq =
   let i           = build_coq_I () in
   let absurd_term = build_coq_False () in
   let eq_elim     = lbeq.ind in
@@ -479,28 +485,28 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
 
 exception NotDiscriminable
 
-let discrEq (lbeq,(t,t1,t2)) id gls =
-  let sort = pf_type_of gls (pf_concl gls) in 
+let eq_baseid = id_of_string "e"
+
+let discr_positions env sigma (lbeq,(t,t1,t2)) id cpath dirn sort =
+  let e = next_ident_away eq_baseid (ids_of_context env) in
+  let e_env = push_named (e,None,t) env in
+  let discriminator =
+    build_discriminator sigma e_env dirn (mkVar e) sort cpath in
+  let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq in
+  tclCOMPLETE 
+    ((tclTHENS (cut_intro absurd_term)
+      [onLastHyp gen_absurdity; 
+       refine (mkApp (pf,[|mkVar id|]))]))
+
+let discrEq (lbeq,(t,t1,t2) as u) id gls =
   let sigma = project gls in
   let env = pf_env gls in
-  (match find_positions env sigma t1 t2 with
-     | Inr _ ->
-	 errorlabstrm "discr" (str" Not a discriminable equality")
-     | Inl (cpath, (_,dirn), _) ->
-	 let e = pf_get_new_id (id_of_string "ee") gls in
-	 let e_env = push_named (e,None,t) env in
-	 let discriminator =
-	   build_discriminator sigma e_env dirn (mkVar e) sort cpath in
-	 let (pf, absurd_term) =
-	   discrimination_pf e (t,t1,t2) discriminator lbeq gls 
-	 in
-	 tclCOMPLETE((tclTHENS (cut_intro absurd_term)
-			([onLastHyp gen_absurdity;
-			  refine (mkApp (pf, [| mkVar id |]))]))) gls)
-
-let not_found_message id =
-  (str "The variable" ++ spc () ++ str (string_of_id id) ++ spc () ++
-    str" was not found in the current environment")
+  match find_positions env sigma t1 t2 with
+    | Inr _ ->
+	errorlabstrm "discr" (str" Not a discriminable equality")
+    | Inl (cpath, (_,dirn), _) ->
+	let sort = pf_apply get_type_of gls (pf_concl gls) in 
+	discr_positions env sigma u id cpath dirn sort gls
 
 let onEquality tac id gls =
   let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
@@ -533,7 +539,7 @@ let discrEverywhere =
   tclORELSE
     (Tacticals.tryAllClauses discrSimpleClause)
     (fun gls -> 
-       errorlabstrm "DiscrEverywhere" (str" No discriminable equalities"))
+       errorlabstrm "DiscrEverywhere" (str"No discriminable equalities"))
 
 let discr_tac = function
   | None -> discrEverywhere
@@ -723,15 +729,9 @@ let make_iterated_tuple env sigma dflt (z,zty) =
 let rec build_injrec sigma env dflt c = function
   | [] -> make_iterated_tuple env sigma dflt (c,type_of env sigma c)
   | ((sp,cnum),argnum)::l ->
-      let cty = type_of env sigma c in
-      let (ity,_) = find_mrectype env sigma cty in
-      let (mib,mip) = lookup_mind_specif env ity in
-      let nparams = mib.mind_nparams in
       let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in
-      let newc = mkRel(cnum_nlams-(argnum-nparams)) in
-      let (subval,tuplety,dfltval) =
-      	build_injrec sigma cnum_env dflt newc l
-      in
+      let newc = mkRel(cnum_nlams-argnum) in
+      let (subval,tuplety,dfltval) = build_injrec sigma cnum_env dflt newc l in
       (kont subval (dfltval,tuplety),
        tuplety,dfltval)
 
@@ -739,6 +739,7 @@ let build_injector sigma env dflt c cpath =
   let (injcode,resty,_) = build_injrec sigma env dflt c cpath in
   (injcode,resty)
 
+(*
 let try_delta_expand env sigma t =
   let whdt = whd_betadeltaiota env sigma t  in 
   let rec hd_rec c  =
@@ -749,12 +750,39 @@ let try_delta_expand env sigma t =
       | _  -> t
   in 
   hd_rec whdt 
+*)
 
 (* Given t1=t2 Inj calculates the whd normal forms of t1 and t2 and it 
    expands then only when the whdnf has a constructor of an inductive type
    in hd position, otherwise delta expansion is not done *)
 
-let injEq (eq,(t,t1,t2)) id gls =
+let simplify_args env sigma t = 
+  (* Quick hack to reduce in arguments of eq only *)
+  match decompose_app t with
+    | eq, [t;c1;c2] -> applist (eq,[t;nf env sigma c1;nf env sigma c2])
+    | eq, [t1;c1;t2;c2] -> applist (eq,[t1;nf env sigma c1;t2;nf env sigma c2])
+    | _ -> t
+
+let inject_at_positions env sigma (eq,(t,t1,t2)) id posns =
+  let e = next_ident_away eq_baseid (ids_of_context env) in
+  let e_env = push_named (e,None,t) env in
+  let injectors =
+    map_succeed
+      (fun (cpath,t1',t2') ->
+        (* arbitrarily take t1' as the injector default value *)
+	let (injbody,resty) = build_injector sigma e_env t1' (mkVar e) cpath in
+	let injfun = mkNamedLambda e t injbody in
+	let pf = applist(eq.congr,[t;resty;injfun;t1;t2;mkVar id]) in
+	let ty = simplify_args env sigma (get_type_of env sigma pf) in
+	(pf,ty))
+      posns in
+  if injectors = [] then
+    errorlabstrm "Equality.inj" (str "Failed to decompose the equality");
+  tclMAP
+    (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf])
+    injectors
+
+let injEq ipats (eq,(t,t1,t2)) id gls =
   let sigma = project gls in
   let env = pf_env gls in
   match find_positions env sigma t1 t2 with
@@ -766,100 +794,38 @@ let injEq (eq,(t,t1,t2)) id gls =
 	errorlabstrm "Equality.inj" 
 	   (str"Nothing to do, it is an equality between convertible terms")
     | Inr posns ->
-	let e = pf_get_new_id (id_of_string "e") gls in
-	let e_env = push_named (e,None,t) env in
-	let injectors =
-	  map_succeed
-	    (fun (cpath,t1_0,t2_0) ->
-	      try 
-		let (injbody,resty) =
-                  (* take arbitrarily t1_0 as the injector default value *)
-		  build_injector sigma e_env t1_0 (mkVar e) cpath in
-		let injfun = mkNamedLambda e t injbody in
-		let _ = type_of env sigma injfun in (injfun,resty)
-	      with e when catchable_exception e ->
-		(* may fail because ill-typed or because of a Prop argument *)
-		(* error "find_sigma_data" *)
-		failwith "caught")
-            posns
-	in
-	if injectors = [] then
-	  errorlabstrm "Equality.inj" 
-	    (str "Failed to decompose the equality");
-	tclMAP 
-	  (fun (injfun,resty) ->
-	     let pf = applist(eq.congr,
-			      [t;resty;injfun;
-			       try_delta_expand env sigma t1;
-			       try_delta_expand env sigma t2;
-			       mkVar id]) 
-	     in
-	     let ty =
-	       try pf_nf gls (pf_type_of gls pf)
-               with
-		 | UserError("refiner__fail",_) -> 
-		     errorlabstrm "InjClause" 
-		(str (string_of_id id) ++ str" Not a projectable equality")
-	     in ((tclTHENS  (cut  ty) ([tclIDTAC;refine pf]))))
-	  injectors
+(* Est-ce utile à partir du moment où les arguments projetés subissent "nf" ?
+	let t1 = try_delta_expand env sigma t1 in
+	let t2 = try_delta_expand env sigma t2 in
+*)
+	tclTHEN 
+	  (inject_at_positions env sigma (eq,(t,t1,t2)) id posns)
+	  (intros_pattern None ipats)
 	  gls
 
-let inj = onEquality injEq
+let inj ipats = onEquality (injEq ipats)
 
-let injClause = function
-  | None -> onNegatedEquality injEq
-  | Some id -> try_intros_until inj id
+let injClause ipats = function
+  | None -> onNegatedEquality (injEq ipats)
+  | Some id -> try_intros_until (inj ipats) id
 
-let injConcl gls  = injClause None gls
-let injHyp id gls = injClause (Some id) gls
+let injConcl gls  = injClause [] None gls
+let injHyp id gls = injClause [] (Some id) gls
 
-let decompEqThen ntac (lbeq,(t,t1,t2)) id gls =
-  let sort = pf_type_of gls (pf_concl gls) in 
+let decompEqThen ntac (lbeq,(t,t1,t2) as u) id gls =
+  let sort = pf_apply get_type_of gls (pf_concl gls) in 
   let sigma = project gls in
   let env = pf_env gls in 
-  (match find_positions env sigma t1 t2 with
-     | Inl (cpath, (_,dirn), _) ->
-	 let e = pf_get_new_id (id_of_string "e") gls in
-	 let e_env = push_named (e,None,t) env in
-	 let discriminator =
-	   build_discriminator sigma e_env dirn (mkVar e) sort cpath in
-	 let (pf, absurd_term) =
-	   discrimination_pf e (t,t1,t2) discriminator lbeq gls in
-	 tclCOMPLETE
-	   ((tclTHENS (cut_intro absurd_term)
-	       ([onLastHyp gen_absurdity;
-		 refine (mkApp (pf, [| mkVar id |]))]))) gls
-     | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
-         ntac 0 gls
-     | Inr posns ->
-	 (let e = pf_get_new_id (id_of_string "e") gls in
-	  let e_env = push_named (e,None,t) env in
-	  let injectors =
-	    map_succeed
-	      (fun (cpath,t1_0,t2_0) ->
-		 let (injbody,resty) =
-                  (* take arbitrarily t1_0 as the injector default value *)
-		   build_injector sigma e_env t1_0 (mkVar e) cpath in
-		 let injfun = mkNamedLambda e t injbody in
-		 try 
-		   let _ = type_of env sigma injfun in (injfun,resty)
-		 with e when catchable_exception e -> failwith "caught")
-	      posns 
-	  in
-	  if injectors = [] then
-	    errorlabstrm "Equality.decompEqThen" 
-              (str "Discriminate failed to decompose the equality");
-	  (tclTHEN
-	      (tclMAP (fun (injfun,resty) ->
-			 let pf = applist(lbeq.congr,
-					  [t;resty;injfun;t1;t2;
-					   mkVar id]) in
-			 let ty = pf_nf gls (pf_type_of gls pf) in
-			 ((tclTHENS (cut ty) 
-			     ([tclIDTAC;refine pf]))))
-		 (List.rev injectors))
-	      (ntac (List.length injectors)))
-	  gls))
+  match find_positions env sigma t1 t2 with
+    | Inl (cpath, (_,dirn), _) ->
+	discr_positions env sigma u id cpath dirn sort gls
+    | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
+        ntac 0 gls
+    | Inr posns ->
+	tclTHEN
+	  (inject_at_positions env sigma (lbeq,(t,t1,t2)) id (List.rev posns))
+	  (ntac (List.length posns))
+	  gls
 
 let dEqThen ntac = function
   | None -> onNegatedEquality (decompEqThen ntac)
@@ -903,7 +869,7 @@ let find_elim sort_of_gl lbeq =
 
 let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
   (* find substitution scheme *)
-  let eq_elim = find_elim (pf_type_of gls (pf_concl gls)) lbeq in
+  let eq_elim = find_elim (pf_apply get_type_of gls (pf_concl gls)) lbeq in
   (* build substitution predicate *)
   let p = lambda_create (pf_env gls) (t,body) in
   (* apply substitution scheme *)
@@ -1013,7 +979,7 @@ let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
 let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
 
 let substClause l2r c cls gls =
-  let eq = pf_type_of gls c in
+  let eq = pf_apply get_type_of gls c in
   tclTHENS (cutSubstClause l2r eq cls) [tclIDTAC; exact_no_check c] gls
 
 let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls)
@@ -1147,28 +1113,10 @@ let subst_all gl =
   let ids = list_uniquize ids in
   subst ids gl
 
+
 (* Rewrite the first assumption for which the condition faildir does not fail 
    and gives the direction of the rewrite *)
 
-let rewrite_assumption_cond faildir gl =
-   let rec arec = function
-      | [] -> error "No such assumption"
-      | (id,_,t)::rest -> 
-	  (try let dir = faildir t gl in 
-	       general_rewrite dir (mkVar id) gl
-	   with Failure _ | UserError _  ->  arec rest)
-   in arec (pf_hyps gl)
-
-
-let rewrite_assumption_cond_in faildir hyp gl =
-   let rec arec = function
-      | [] -> error "No such assumption"
-      | (id,_,t)::rest -> 
-	  (try let dir = faildir t gl in 
-	       general_rewrite_in dir hyp (mkVar id) gl
-	   with Failure _ | UserError _ ->  arec rest)
-   in arec (pf_hyps gl)
-
 let cond_eq_term_left c t gl =
   try
     let (_,x,_) = snd (find_eq_data_decompose t) in
@@ -1189,6 +1137,48 @@ let cond_eq_term c t gl =
     else failwith "not convertible"
   with PatternMatchingFailure -> failwith "not an equality"
 
+let rewrite_mutli_assumption_cond cond_eq_term cl gl = 
+  let rec arec = function 
+    | [] -> error "No such assumption"
+    | (id,_,t) ::rest -> 
+	begin 
+	  try 
+	    let dir = cond_eq_term t gl in 
+	    general_multi_rewrite dir (mkVar id,NoBindings) cl gl
+	  with | Failure _ | UserError _ -> arec rest
+	end
+  in 
+  arec (pf_hyps gl)
+
+let replace_multi_term dir_opt c  = 
+  let cond_eq_fun = 
+    match dir_opt with 
+      | None -> cond_eq_term c
+      | Some true -> cond_eq_term_left c
+      | Some false -> cond_eq_term_right c
+  in 
+  rewrite_mutli_assumption_cond cond_eq_fun 
+
+(* JF. old version 
+let rewrite_assumption_cond faildir gl =
+   let rec arec = function
+      | [] -> error "No such assumption"
+      | (id,_,t)::rest ->
+	  (try let dir = faildir t gl in
+	       general_rewrite dir (mkVar id) gl
+	   with Failure _ | UserError _  ->  arec rest)
+   in arec (pf_hyps gl)
+
+
+let rewrite_assumption_cond_in faildir hyp gl =
+   let rec arec = function
+      | [] -> error "No such assumption"
+      | (id,_,t)::rest ->
+	  (try let dir = faildir t gl in
+	       general_rewrite_in dir hyp (mkVar id) gl
+	   with Failure _ | UserError _ ->  arec rest)
+   in arec (pf_hyps gl)
+
 let replace_term_left t = rewrite_assumption_cond (cond_eq_term_left t)
 
 let replace_term_right t = rewrite_assumption_cond (cond_eq_term_right t)
@@ -1200,6 +1190,27 @@ let replace_term_in_left t = rewrite_assumption_cond_in (cond_eq_term_left t)
 let replace_term_in_right t = rewrite_assumption_cond_in (cond_eq_term_right t)
    
 let replace_term_in t = rewrite_assumption_cond_in (cond_eq_term t)
+*)
+
+let replace_term_left t = replace_multi_term (Some true) t Tacticals.onConcl
+
+let replace_term_right t = replace_multi_term (Some false) t Tacticals.onConcl
+
+let replace_term t = replace_multi_term None t Tacticals.onConcl
+
+let replace_term_in_left t hyp = replace_multi_term (Some true) t (Tacticals.onHyp hyp)
+
+let replace_term_in_right t hyp = replace_multi_term (Some false) t (Tacticals.onHyp hyp)
+
+let replace_term_in t hyp = replace_multi_term None t (Tacticals.onHyp hyp)
+
+
+
+
+
+
+
+
 
-let _ = Setoid_replace.register_replace replace
+let _ = Setoid_replace.register_replace (fun tac_opt c2 c1 gl ->  replace_in_clause_maybe_by c2 c1 onConcl tac_opt gl)
 let _ = Setoid_replace.register_general_rewrite general_rewrite
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 9ee565c5..3d6a08b6 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 8780 2006-05-02 21:58:58Z letouzey $ i*)
+(*i $Id: equality.mli 9195 2006-10-01 09:41:57Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -22,6 +22,7 @@ open Tacticals
 open Tactics
 open Tacexpr
 open Rawterm
+open Genarg
 (*i*)
 
 val general_rewrite_bindings : bool -> constr with_bindings -> tactic
@@ -50,19 +51,21 @@ val conditional_rewrite : bool -> tactic -> constr with_bindings -> tactic
 val conditional_rewrite_in :
   bool -> identifier -> tactic -> constr with_bindings -> tactic
 
+val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic
 val replace    : constr -> constr -> tactic
 val replace_in : identifier -> constr -> constr -> tactic
-val replace_by : constr -> constr -> tactic -> tactic 
-val replace_in_by : identifier -> constr -> constr -> tactic -> tactic 
-val new_replace : constr -> constr -> identifier option -> tactic option -> tactic
+val replace_by : constr -> constr -> tactic -> tactic
+val replace_in_by : identifier -> constr -> constr -> tactic -> tactic
+
 val discr        : identifier -> tactic
 val discrConcl   : tactic
 val discrClause  : clause -> tactic
 val discrHyp     : identifier -> tactic
 val discrEverywhere     : tactic
 val discr_tac    : quantified_hypothesis option -> tactic
-val inj          : identifier -> tactic
-val injClause    : quantified_hypothesis option -> tactic
+val inj          : intro_pattern_expr list -> identifier -> tactic
+val injClause    : intro_pattern_expr list -> quantified_hypothesis option ->
+                   tactic
 
 val dEq : quantified_hypothesis option -> tactic
 val dEqThen : (int -> tactic) -> quantified_hypothesis option -> tactic
@@ -111,9 +114,8 @@ val subst : identifier list -> tactic
 val subst_all : tactic
 
 (* Replace term *)
-val replace_term_left : constr -> tactic
-val replace_term_right : constr -> tactic
-val replace_term : constr -> tactic
-val replace_term_in_left : constr -> identifier -> tactic
-val replace_term_in_right : constr -> identifier -> tactic
-val replace_term_in : constr -> identifier -> tactic
+(* [replace_multi_term dir_opt c cl] 
+   perfoms replacement of [c] by the first value found in context
+   (according to [dir] if given to get the rewrite direction)  in the clause [cl]
+*)
+val replace_multi_term : bool option -> constr -> clause -> tactic
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 31c060f1..ed40af1c 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 8759 2006-04-28 12:24:14Z herbelin $ *)
+(* $Id: evar_tactics.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
 
 open Term
 open Util
@@ -51,7 +51,7 @@ let instantiate n rawc ido gl =
       error "not enough uninstantiated existential variables";
     if n <= 0 then error "incorrect existential variable index";
     let ev,_ =  destEvar (List.nth evl (n-1)) in
-    let evd' = w_refine (pf_env gl) ev rawc (create_evar_defs sigma)  in
+    let evd' = w_refine ev rawc (create_evar_defs sigma)  in
     Refiner.tclEVARS (evars_of evd') gl
 	
 (*
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 5a0b4b8c..3c7d76b2 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: extraargs.ml4 8739 2006-04-26 22:23:37Z herbelin $ *)
+(* $Id: extraargs.ml4 9076 2006-08-23 15:05:54Z jforest $ *)
 
 open Pp
 open Pcoq
@@ -124,3 +124,115 @@ ARGUMENT EXTEND hloc
    
  END
 
+
+
+
+
+
+
+(* Julien: Mise en commun des differentes version de replace with in by *)
+
+let pr_by_arg_tac _prc _prlc prtac opt_c = 
+  match opt_c with 
+    | None -> mt ()
+    | Some t -> spc () ++ hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t)
+
+ARGUMENT EXTEND by_arg_tac
+  TYPED AS tactic_opt
+  PRINTED BY pr_by_arg_tac
+| [ "by" tactic3(c) ] -> [ Some c ]
+| [ ] -> [ None ]
+END
+ 
+
+let pr_in_hyp  pr_id (lo,concl) :  Pp.std_ppcmds = 
+  match lo,concl with 
+    | Some [],true -> mt ()
+    | None,true -> str "in" ++ spc () ++ str "*"
+    | None,false -> str "in" ++ spc () ++ str "*" ++ spc () ++ str "|-" 
+    | Some l,_ -> 
+	str "in" ++ spc () ++ 
+	  Util.prlist_with_sep spc pr_id l ++ 
+	  match concl with 
+	    | true -> spc () ++ str "|-" ++ spc () ++ str "*"
+	    | _ -> mt ()
+
+
+let pr_in_arg_hyp _ _ _ = pr_in_hyp (fun (_,id) -> Ppconstr.pr_id id)
+
+let pr_in_arg_hyp_typed  _ _  _  = pr_in_hyp Ppconstr.pr_id 
+
+
+let pr_var_list_gen pr_id = Util.prlist_with_sep (fun () -> str ",") pr_id 
+
+let pr_var_list_typed _ _ _ =  pr_var_list_gen Ppconstr.pr_id 
+
+let pr_var_list _ _ _ = pr_var_list_gen (fun (_,id) -> Ppconstr.pr_id id)
+
+
+ARGUMENT EXTEND comma_var_lne 
+  TYPED AS var list 
+  PRINTED BY pr_var_list_typed
+  RAW_TYPED AS var list 
+  RAW_PRINTED BY pr_var_list
+  GLOB_TYPED AS var list
+  GLOB_PRINTED BY pr_var_list
+| [ var(x) ] -> [ [x] ]
+| [ var(x) "," comma_var_lne(l) ] -> [x::l]
+END
+
+ARGUMENT EXTEND comma_var_l 
+  TYPED AS var list 
+  PRINTED BY pr_var_list_typed
+  RAW_TYPED AS var list 
+  RAW_PRINTED BY pr_var_list
+  GLOB_TYPED AS var list
+  GLOB_PRINTED BY pr_var_list
+| [  comma_var_lne(l) ] -> [l]
+| [] -> [ [] ]
+END
+
+let pr_in_concl _ _ _ = function true -> str "|- " ++ spc () ++ str "*" | _ -> str "|-" 
+
+ARGUMENT EXTEND inconcl  
+  TYPED AS bool 
+  PRINTED BY pr_in_concl
+| [ "|-" "*" ] -> [ true ]
+| [ "|-" ] -> [ false ]
+END
+
+
+
+ARGUMENT EXTEND in_arg_hyp
+  TYPED AS var list option * bool
+  PRINTED BY pr_in_arg_hyp_typed
+  RAW_TYPED AS var list option * bool 
+  RAW_PRINTED BY pr_in_arg_hyp
+  GLOB_TYPED AS var list option * bool
+  GLOB_PRINTED BY pr_in_arg_hyp
+| [ "in" "*" ] -> [(None,true)]
+| [ "in" "*" inconcl_opt(b) ] -> [let onconcl = match b with Some b -> b | None -> true in (None,onconcl)]
+| [ "in" comma_var_l(l) inconcl_opt(b) ] -> [ let onconcl = match b with Some b -> b | None -> false in 
+					      Some l, onconcl
+					   ]
+| [ ] -> [ (Some [],true) ]
+END
+
+
+let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause = 
+  {Tacexpr.onhyps=
+   Util.option_map 
+     (fun l -> 
+	List.map 
+	  (fun id -> ( ([],trad_id id) ,Tacexpr.InHyp))
+	  l
+     )
+     hyps;
+   Tacexpr.onconcl=concl;
+   Tacexpr.concl_occs = []}
+
+
+let raw_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause snd 
+let glob_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause (fun x -> x) 
+
+
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 004fef02..4a9a0c5f 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extraargs.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
+(*i $Id: extraargs.mli 9076 2006-08-23 15:05:54Z jforest $ i*)
 
 open Tacexpr
 open Term
@@ -39,3 +39,14 @@ val rawwit_hloc : loc_place raw_abstract_argument_type
 val wit_hloc : place closed_abstract_argument_type
 val hloc : loc_place Pcoq.Gram.Entry.e
 
+
+val in_arg_hyp:  (Names.identifier Util.located list option * bool)  Pcoq.Gram.Entry.e
+val rawwit_in_arg_hyp : (Names.identifier Util.located list option * bool) raw_abstract_argument_type
+val wit_in_arg_hyp : (Names.identifier list option * bool) closed_abstract_argument_type
+val raw_in_arg_hyp_to_clause : (Names.identifier Util.located list option * bool) -> Tacticals.clause
+val glob_in_arg_hyp_to_clause :  (Names.identifier list option * bool)  -> Tacticals.clause
+
+
+val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.Entry.e
+val rawwit_by_arg_tac :  raw_tactic_expr option raw_abstract_argument_type
+val wit_by_arg_tac : glob_tactic_expr option closed_abstract_argument_type
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index c2820c44..a8204665 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: extratactics.ml4 8979 2006-06-23 10:17:14Z herbelin $ *)
+(* $Id: extratactics.ml4 9266 2006-10-24 09:03:15Z herbelin $ *)
 
 open Pp
 open Pcoq
@@ -20,116 +20,25 @@ 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]
-END
-
-TACTIC EXTEND rewrite_in
-| [ "rewrite" orient(b) constr_with_bindings(c) "in" hyp(h) ] ->
-    [general_rewrite_bindings_in b h c]
-END
-
-let h_rewriteLR x = h_rewrite true (x,Rawterm.NoBindings) 
-*)
-
-(* Julien: Mise en commun des differentes version de replace with in by 
-   TODO: deplacer dans extraargs
-
-*)
-
-let pr_by_arg_tac _prc _prlc prtac opt_c = 
-  match opt_c with 
-    | None -> mt ()
-    | Some t -> spc () ++ hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t)
-
-let pr_in_hyp = function
-  | None -> mt ()
-  | Some id -> spc () ++ hov 2 (str "in" ++ spc () ++ Nameops.pr_id id)
-
-let pr_in_arg_hyp _prc _prlc _prtac opt_c =
-  pr_in_hyp (Util.option_map snd opt_c)
-
-let pr_in_arg_hyp_typed _prc _prlc _prtac =
-  pr_in_hyp
-
-ARGUMENT EXTEND by_arg_tac
-  TYPED AS tactic_opt
-  PRINTED BY pr_by_arg_tac
-| [ "by" tactic3(c) ] -> [ Some c ]
-| [ ] -> [ None ]
-END
- 
-ARGUMENT EXTEND in_arg_hyp
-  TYPED AS var_opt
-  PRINTED BY pr_in_arg_hyp_typed
-  RAW_TYPED AS var_opt
-  RAW_PRINTED BY pr_in_arg_hyp
-  GLOB_TYPED AS var_opt
-  GLOB_PRINTED BY pr_in_arg_hyp
-| [ "in" hyp(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_map Tacinterp.eval_tactic tac) ]
-END
-
-(* Julien:
-  old version  
-
-TACTIC EXTEND replace
-| [ "replace" constr(c1) "with" constr(c2) ] ->
-    [ replace c1 c2 ]
-END
-
-TACTIC EXTEND replace_by
-|  [ "replace" constr(c1) "with" constr(c2) "by" tactic(tac) ] ->
-    [ replace_by c1 c2 (snd tac)  ]
- 
-END
-
-TACTIC EXTEND replace_in
-| [ "replace" constr(c1) "with" constr(c2) "in" hyp(h) ] ->
-    [ replace_in h c1 c2 ]
-END
-
-TACTIC EXTEND replace_in_by
-| [ "replace" constr(c1) "with" constr(c2) "in" hyp(h) "by" tactic(tac) ] ->
-    [ replace_in_by h c1 c2 (snd tac) ]
+-> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) (Util.option_map Tacinterp.eval_tactic tac) ]
 END
 
-*)
-
 TACTIC EXTEND replace_term_left
-  [ "replace" "->" constr(c)  ] -> [ replace_term_left c ]
+  [ "replace"  "->" constr(c) in_arg_hyp(in_hyp) ]
+  -> [ replace_multi_term (Some true) c (glob_in_arg_hyp_to_clause in_hyp)]
 END
 
 TACTIC EXTEND replace_term_right
-  [ "replace" "<-" constr(c)  ] -> [ replace_term_right c ]
+  [ "replace"  "<-" constr(c) in_arg_hyp(in_hyp) ]
+  -> [replace_multi_term (Some false) c (glob_in_arg_hyp_to_clause in_hyp)]
 END
 
 TACTIC EXTEND replace_term
-  [ "replace" constr(c)  ] -> [ replace_term c ]
-END
-
-TACTIC EXTEND replace_term_in_left
-  [ "replace"  "->" constr(c) "in" hyp(h) ]
-  -> [ replace_term_in_left c h ]
-END
-
-TACTIC EXTEND replace_term_in_right
-  [ "replace"  "<-" constr(c) "in" hyp(h) ]
-  -> [ replace_term_in_right c h ]
-END
-
-TACTIC EXTEND replace_term_in
-  [ "replace" constr(c) "in" hyp(h) ]
-  -> [ replace_term_in c h ]
+  [ "replace" constr(c) in_arg_hyp(in_hyp) ]
+  -> [ replace_multi_term None c (glob_in_arg_hyp_to_clause in_hyp) ]
 END
 
 TACTIC EXTEND simplify_eq
@@ -143,7 +52,11 @@ END
 let h_discrHyp id = h_discriminate (Some id)
 
 TACTIC EXTEND injection
-  [ "injection" quantified_hypothesis_opt(h) ] -> [ injClause h ]
+  [ "injection" quantified_hypothesis_opt(h) ] -> [ injClause [] h ]
+END 
+TACTIC EXTEND injection_as
+  [ "injection" quantified_hypothesis_opt(h) 
+    "as" simple_intropattern_list(ipat)] -> [ injClause ipat h ]
 END
 
 let h_injHyp id = h_injection (Some id)
@@ -182,7 +95,7 @@ END
 (* AutoRewrite *)
 
 open Autorewrite
-
+(* J.F : old version 
 TACTIC EXTEND autorewrite
   [ "autorewrite" "with" ne_preident_list(l) ] ->
     [ autorewrite Refiner.tclIDTAC l ]
@@ -193,6 +106,21 @@ TACTIC EXTEND autorewrite
 | [ "autorewrite" "with" ne_preident_list(l) "in" hyp(id) "using" tactic(t) ] ->
     [ autorewrite_in id (snd t) l ]
 END
+*)
+
+TACTIC EXTEND autorewrite
+| [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) ] ->
+    [ auto_multi_rewrite  l (glob_in_arg_hyp_to_clause  cl) ]
+| [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) "using" tactic(t) ] ->
+    [ 
+      let cl =  glob_in_arg_hyp_to_clause cl in 
+      auto_multi_rewrite_with (snd t) l cl
+
+    ]
+END
+
+
+
 
 let add_rewrite_hint name ort t lcsr =
   let env = Global.env() and sigma = Evd.empty in
@@ -223,22 +151,22 @@ let refine_tac = h_refine
 open Setoid_replace
 
 TACTIC EXTEND setoid_replace
-   [ "setoid_replace" constr(c1) "with" constr(c2) ] ->
-     [ setoid_replace None c1 c2 ~new_goals:[] ]
- | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel)] ->
-     [ setoid_replace (Some rel) c1 c2 ~new_goals:[] ]
- | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) ] ->
-     [ setoid_replace None c1 c2 ~new_goals:l ]
- | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) ] ->
-     [ setoid_replace (Some rel) c1 c2 ~new_goals:l ]
- | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) ] ->
-     [ setoid_replace_in h None c1 c2 ~new_goals:[] ]
- | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel)] ->
-     [ setoid_replace_in h (Some rel) c1 c2 ~new_goals:[] ]
- | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] ->
-     [ setoid_replace_in h None c1 c2 ~new_goals:l ]
- | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) ] ->
-     [ setoid_replace_in h (Some rel) c1 c2 ~new_goals:l ]
+   [ "setoid_replace" constr(c1) "with" constr(c2) by_arg_tac(tac)] ->
+     [ setoid_replace  (Util.option_map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ]
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) by_arg_tac(tac)] ->
+     [ setoid_replace  (Util.option_map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ]
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] ->
+     [ setoid_replace  (Util.option_map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ]
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] ->
+     [ setoid_replace  (Util.option_map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ]
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) by_arg_tac(tac) ] ->
+     [ setoid_replace_in  (Util.option_map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ]
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) by_arg_tac(tac)] ->
+     [ setoid_replace_in  (Util.option_map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ]
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] ->
+     [ setoid_replace_in  (Util.option_map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ]
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] ->
+     [ setoid_replace_in  (Util.option_map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ]
 END
 
 TACTIC EXTEND setoid_rewrite
@@ -471,3 +399,9 @@ VERNAC COMMAND EXTEND ImplicitTactic
 | [ "Declare" "Implicit" "Tactic" tactic(tac) ] ->
     [ Tacinterp.declare_implicit_tactic (Tacinterp.interp tac) ]
 END
+
+TACTIC EXTEND apply_in
+| ["apply" constr_with_bindings(c) "in" hyp(id) ] -> [ apply_in id [c] ]
+| ["apply" constr_with_bindings(c) "," constr_with_bindings_list_sep(cl,",") 
+   "in" hyp(id) ] -> [ apply_in id (c::cl) ]
+END
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 91766254..234c0161 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 8977 2006-06-23 10:09:59Z herbelin $ i*)
+(*i $Id: extratactics.mli 9073 2006-08-22 08:54:29Z jforest $ i*)
 
 open Util
 open Names
@@ -22,21 +22,3 @@ val h_injHyp : quantified_hypothesis -> tactic
 
 val refine_tac : Genarg.open_constr -> tactic
 
-
-
-(* Julien: Mise en commun des differentes version de replace with in by 
-   TODO:  deplacer dans extraargs
-
-*)
-
-
-val rawwit_in_arg_hyp: identifier located option raw_abstract_argument_type
-
-val in_arg_hyp: identifier located option Pcoq.Gram.Entry.e
-
-
-
-val rawwit_by_arg_tac :
-  (raw_tactic_expr option, constr_expr, raw_tactic_expr) abstract_argument_type
-  
-val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.Entry.e
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 7974ce56..9507ce5f 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: leminv.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
+(* $Id: leminv.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
 
 open Pp
 open Util
@@ -217,7 +217,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     (str"Computed inversion goal was not closed in initial signature");
   *)
   let invSign = named_context_val invEnv in
-  let pfs = mk_pftreestate (mk_goal invSign invGoal) in
+  let pfs = mk_pftreestate (mk_goal invSign invGoal None) in
   let pfs = solve_pftreestate (tclTHEN intro (onLastHyp inv_op)) pfs in
   let (pfterm,meta_types) = extract_open_pftreestate pfs in
   let global_named_context = Global.named_context () in
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 8c8d4d37..2727e669 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 8900 2006-06-06 14:40:27Z letouzey $ *)
+(* $Id: setoid_replace.ml 9331 2006-11-01 09:36:06Z herbelin $ *)
 
 open Tacmach
 open Proof_type
@@ -33,7 +33,7 @@ open Decl_kinds
 open Constrintern
 open Mod_subst
 
-let replace = ref (fun _ _ -> assert false)
+let replace = ref (fun _ _ _ -> assert false)
 let register_replace f = replace := f
 
 let general_rewrite = ref (fun _ _ -> assert false)
@@ -155,7 +155,7 @@ let coq_MSCovariant = lazy(constant ["Setoid"] "MSCovariant")
 let coq_MSContravariant = lazy(constant ["Setoid"] "MSContravariant")
 
 let coq_singl = lazy(constant ["Setoid"] "singl")
-let coq_cons = lazy(constant ["Setoid"] "cons")
+let coq_cons = lazy(constant ["Setoid"] "necons")
 
 let coq_equality_morphism_of_asymmetric_areflexive_transitive_relation =
  lazy(constant ["Setoid"]
@@ -805,135 +805,140 @@ let new_morphism m signature id hook =
   let typeofm = Typing.type_of env Evd.empty m in
   let typ = clos_norm_flags Closure.betaiotazeta empty_env Evd.empty typeofm in
   let argsrev, output =
-   match signature with
-      None -> decompose_prod typ
-    | Some (_,output') ->
-       (* the carrier of the relation output' can be a Prod ==>
-          we must uncurry on the fly output.
-          E.g: A -> B -> C vs        A -> (B -> C)
-                args   output     args     output
-       *)
-       let rel = find_relation_class output' in
-       let rel_a,rel_quantifiers_no =
-        match rel with
-           Relation rel -> rel.rel_a, rel.rel_quantifiers_no
-         | Leibniz (Some t) -> t, 0
-         | Leibniz None -> assert false in
-       let rel_a_n =
-        clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a in
-       try
-        let _,output_rel_a_n = decompose_lam_n rel_quantifiers_no rel_a_n in
-        let argsrev,_ = decompose_prod output_rel_a_n in
-        let n = List.length argsrev in
-        let argsrev',_ = decompose_prod typ in
-        let m = List.length argsrev' in
-         decompose_prod_n (m - n) typ
-       with UserError(_,_) ->
-        (* decompose_lam_n failed. This may happen when rel_a is an axiom,
-           a constructor, an inductive type, etc. *)
-        decompose_prod typ
+    match signature with
+	None -> decompose_prod typ
+      | Some (_,output') ->
+	  (* the carrier of the relation output' can be a Prod ==>
+             we must uncurry on the fly output.
+             E.g: A -> B -> C vs        A -> (B -> C)
+             args   output     args     output
+	  *)
+	  let rel = 
+	    try find_relation_class output' 
+	    with Not_found -> errorlabstrm "Add Morphism"
+	      (str "Not a valid signature: " ++ pr_lconstr output' ++
+		  str " is neither a registered relation nor the Leibniz " ++
+		  str " equality.") in
+	  let rel_a,rel_quantifiers_no =
+            match rel with
+		Relation rel -> rel.rel_a, rel.rel_quantifiers_no
+              | Leibniz (Some t) -> t, 0
+              | Leibniz None -> assert false in
+	  let rel_a_n =
+            clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a in
+	    try
+              let _,output_rel_a_n = decompose_lam_n rel_quantifiers_no rel_a_n in
+              let argsrev,_ = decompose_prod output_rel_a_n in
+              let n = List.length argsrev in
+              let argsrev',_ = decompose_prod typ in
+              let m = List.length argsrev' in
+		decompose_prod_n (m - n) typ
+	    with UserError(_,_) ->
+              (* decompose_lam_n failed. This may happen when rel_a is an axiom,
+		 a constructor, an inductive type, etc. *)
+              decompose_prod typ
   in
   let args_ty = List.rev argsrev in
   let args_ty_len = List.length (args_ty) in
   let args_ty_quantifiers_rev,args,args_instance,output,output_instance =
-   match signature with
-      None ->
-       if args_ty = [] then
-        errorlabstrm "New Morphism"
-         (str "The term " ++ pr_lconstr m ++ str " has type " ++
-          pr_lconstr typeofm ++ str " that is not a product.") ;
-       ignore (check_is_dependent 0 args_ty output) ;
-       let args =
-        List.map
-         (fun (_,ty) -> None,default_relation_for_carrier ty) args_ty in
-       let output = default_relation_for_carrier output in
-        [],args,args,output,output
-    | Some (args,output') ->
-       assert (args <> []);
-       let number_of_arguments = List.length args in
-       let number_of_quantifiers = args_ty_len - number_of_arguments in
-       if number_of_quantifiers < 0 then
-        errorlabstrm "New Morphism"
-         (str "The morphism " ++ pr_lconstr m ++ str " has type " ++
-          pr_lconstr typeofm ++ str " that attends at most " ++ int args_ty_len ++
-          str " arguments. The signature that you specified requires " ++
-          int number_of_arguments ++ str " arguments.")
-       else
-        begin
-         (* the real_args_ty returned are already delifted *)
-         let args_ty_quantifiers_rev, real_args_ty, real_output =
-          check_is_dependent number_of_quantifiers args_ty output in
-         let quantifiers_rel_context =
-          List.map (fun (n,t) -> n,None,t) args_ty_quantifiers_rev in
-         let env = push_rel_context quantifiers_rel_context env in
-         let find_relation_class t real_t =
-          try
-           let rel = find_relation_class t in
-            rel, unify_relation_class_carrier_with_type env rel real_t
-          with Not_found ->
-           errorlabstrm "Add Morphism"
-            (str "Not a valid signature: " ++ pr_lconstr t ++
-             str " is neither a registered relation nor the Leibniz " ++
-             str " equality.")
-         in
-         let find_relation_class_v (variance,t) real_t =
-          let relation,relation_instance = find_relation_class t real_t in
-           match relation, variance with
-              Leibniz _, None
-            | Relation {rel_sym = Some _}, None
-            | Relation {rel_sym = None}, Some _ ->
-               (variance, relation), (variance, relation_instance)
-            | Relation {rel_sym = None},None ->
-               errorlabstrm "Add Morphism"
-                (str "You must specify the variance in each argument " ++
-                 str "whose relation is asymmetric.")
-            | Leibniz _, Some _
-            | Relation {rel_sym = Some _}, Some _ ->
-               errorlabstrm "Add Morphism"
-                (str "You cannot specify the variance of an argument " ++
-                 str "whose relation is symmetric.")
-         in
-          let args, args_instance =
-           List.split
-            (List.map2 find_relation_class_v args real_args_ty) in
-          let output,output_instance= find_relation_class output' real_output in
-           args_ty_quantifiers_rev, args, args_instance, output, output_instance
-        end
+    match signature with
+	None ->
+	  if args_ty = [] then
+            errorlabstrm "New Morphism"
+              (str "The term " ++ pr_lconstr m ++ str " has type " ++
+		  pr_lconstr typeofm ++ str " that is not a product.") ;
+	  ignore (check_is_dependent 0 args_ty output) ;
+	  let args =
+            List.map
+              (fun (_,ty) -> None,default_relation_for_carrier ty) args_ty in
+	  let output = default_relation_for_carrier output in
+            [],args,args,output,output
+      | Some (args,output') ->
+	  assert (args <> []);
+	  let number_of_arguments = List.length args in
+	  let number_of_quantifiers = args_ty_len - number_of_arguments in
+	    if number_of_quantifiers < 0 then
+              errorlabstrm "New Morphism"
+		(str "The morphism " ++ pr_lconstr m ++ str " has type " ++
+		    pr_lconstr typeofm ++ str " that attends at most " ++ int args_ty_len ++
+		    str " arguments. The signature that you specified requires " ++
+		    int number_of_arguments ++ str " arguments.")
+	    else
+              begin
+		(* the real_args_ty returned are already delifted *)
+		let args_ty_quantifiers_rev, real_args_ty, real_output =
+		  check_is_dependent number_of_quantifiers args_ty output in
+		let quantifiers_rel_context =
+		  List.map (fun (n,t) -> n,None,t) args_ty_quantifiers_rev in
+		let env = push_rel_context quantifiers_rel_context env in
+		let find_relation_class t real_t =
+		  try
+		    let rel = find_relation_class t in
+		      rel, unify_relation_class_carrier_with_type env rel real_t
+		  with Not_found ->
+		    errorlabstrm "Add Morphism"
+		      (str "Not a valid signature: " ++ pr_lconstr t ++
+			  str " is neither a registered relation nor the Leibniz " ++
+			  str " equality.")
+		in
+		let find_relation_class_v (variance,t) real_t =
+		  let relation,relation_instance = find_relation_class t real_t in
+		    match relation, variance with
+			Leibniz _, None
+		      | Relation {rel_sym = Some _}, None
+		      | Relation {rel_sym = None}, Some _ ->
+			  (variance, relation), (variance, relation_instance)
+		      | Relation {rel_sym = None},None ->
+			  errorlabstrm "Add Morphism"
+			    (str "You must specify the variance in each argument " ++
+				str "whose relation is asymmetric.")
+		      | Leibniz _, Some _
+		      | Relation {rel_sym = Some _}, Some _ ->
+			  errorlabstrm "Add Morphism"
+			    (str "You cannot specify the variance of an argument " ++
+				str "whose relation is symmetric.")
+		in
+		let args, args_instance =
+		  List.split
+		    (List.map2 find_relation_class_v args real_args_ty) in
+		let output,output_instance= find_relation_class output' real_output in
+		  args_ty_quantifiers_rev, args, args_instance, output, output_instance
+              end
   in
-   let argsconstr,outputconstr,lem =
+  let argsconstr,outputconstr,lem =
     gen_compat_lemma_statement args_ty_quantifiers_rev output_instance
-     args_instance (apply_to_rels m args_ty_quantifiers_rev) in
-   (* "unfold make_compatibility_goal" *)
-   let lem =
+      args_instance (apply_to_rels m args_ty_quantifiers_rev) in
+    (* "unfold make_compatibility_goal" *)
+  let lem =
     Reductionops.clos_norm_flags
-     (Closure.unfold_red (Lazy.force coq_make_compatibility_goal_eval_ref))
-     env Evd.empty lem in
-   (* "unfold make_compatibility_goal_aux" *)
-   let lem =
+      (Closure.unfold_red (Lazy.force coq_make_compatibility_goal_eval_ref))
+      env Evd.empty lem in
+    (* "unfold make_compatibility_goal_aux" *)
+  let lem =
     Reductionops.clos_norm_flags
-     (Closure.unfold_red(Lazy.force coq_make_compatibility_goal_aux_eval_ref))
-     env Evd.empty lem in
-   (* "simpl" *)
-   let lem = Tacred.nf env Evd.empty lem in
+      (Closure.unfold_red(Lazy.force coq_make_compatibility_goal_aux_eval_ref))
+      env Evd.empty lem in
+    (* "simpl" *)
+  let lem = Tacred.nf env Evd.empty lem in
     if Lib.is_modtype () then
-     begin
-      ignore
-       (Declare.declare_internal_constant id
-        (ParameterEntry lem, IsAssumption Logical)) ;
-      let mor_name = morphism_theory_id_of_morphism_proof_id id in
-      let lemma_infos = Some (id,argsconstr,outputconstr) in
-       add_morphism lemma_infos mor_name
-        (m,args_ty_quantifiers_rev,args,output)
-     end
+      begin
+	ignore
+	  (Declare.declare_internal_constant id
+              (ParameterEntry lem, IsAssumption Logical)) ;
+	let mor_name = morphism_theory_id_of_morphism_proof_id id in
+	let lemma_infos = Some (id,argsconstr,outputconstr) in
+	  add_morphism lemma_infos mor_name
+            (m,args_ty_quantifiers_rev,args,output)
+      end
     else
-     begin
-      new_edited id
-       (m,args_ty_quantifiers_rev,args,argsconstr,output,outputconstr);
-      Pfedit.start_proof id (Global, Proof Lemma) 
-       (Declare.clear_proofs (Global.named_context ()))
-       lem hook;
-      Options.if_verbose msg (Printer.pr_open_subgoals ());
-     end
+      begin
+	new_edited id
+	  (m,args_ty_quantifiers_rev,args,argsconstr,output,outputconstr);
+	Pfedit.start_proof id (Global, Proof Lemma) 
+	  (Declare.clear_proofs (Global.named_context ()))
+	  lem hook;
+	Options.if_verbose msg (Printer.pr_open_subgoals ());
+      end
 
 let morphism_hook _ ref =
   let pf_id = id_of_global ref in
@@ -1272,7 +1277,7 @@ let relation_class_that_matches_a_constr caller_name new_goals hypt =
     forall x1 x2, rel1 x1 x2 -> rel2 x1 x2
    The Coq part of the tactic, however, needs rel1 == rel2.
    Hence the third case commented out.
-   Note: accepting user-defined subtrelations seems to be the last
+   Note: accepting user-defined subrelations seems to be the last
    useful generalization that does not go against the original spirit of
    the tactic.
 *)
@@ -1351,9 +1356,9 @@ let cartesian_product gl a =
    (aux (List.map (elim_duplicates gl identity) (Array.to_list a)))
 
 let mark_occur gl ~new_goals t in_c input_relation input_direction =
- let rec aux output_relation output_direction in_c =
+ let rec aux output_relation output_directions in_c =
   if eq_constr t in_c then
-   if input_direction = output_direction
+   if List.mem input_direction output_directions
    && subrelation gl input_relation output_relation then
     [ToReplace]
    else []
@@ -1400,33 +1405,32 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction =
             (fun res (mor,c,al) ->
               let a =
                let arguments = Array.of_list mor.args in
-               let apply_variance_to_direction default_dir =
+               let apply_variance_to_direction =
                 function
-                   None -> default_dir
-                 | Some true -> output_direction
-                 | Some false -> opposite_direction output_direction
+                   None -> [Left2Right;Right2Left]
+                 | Some true -> output_directions
+                 | Some false -> List.map opposite_direction output_directions
                in
                 Util.array_map2
                  (fun a (variance,relation) ->
-                   (aux relation
-                     (apply_variance_to_direction Left2Right variance) a) @
-                   (aux relation
-                     (apply_variance_to_direction Right2Left variance) a)
+                   (aux relation (apply_variance_to_direction variance) a)
                  ) al arguments
               in
                let a' = cartesian_product gl a in
+	       List.flatten (List.map (fun output_direction ->
                 (List.map
                   (function a ->
                     if not (get_mark a) then
                      ToKeep (in_c,output_relation,output_direction)
                     else
-                     MApp (c,ACMorphism mor,a,output_direction)) a') @ res
+                     MApp (c,ACMorphism mor,a,output_direction)) a'))
+		 output_directions) @ res
             ) [] mors_and_cs_and_als in
           (* Then we look for well typed functions *)
           let res_functions =
            (* the tactic works only if the function type is
                made of non-dependent products only. However, here we
-               can cheat a bit by partially istantiating c to match
+               can cheat a bit by partially instantiating c to match
                the requirement when the arguments to be replaced are
                bound by non-dependent products only. *)
             let typeofc = Tacmach.pf_type_of gl c in
@@ -1437,7 +1441,9 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction =
              function
                 [] ->
                  if a_rev = [] then
-                  [ToKeep (in_c,output_relation,output_direction)]
+		  List.map (fun output_direction ->
+                   ToKeep (in_c,output_relation,output_direction))
+		   output_directions
                  else
                   let a' =
                    cartesian_product gl (Array.of_list (List.rev a_rev))
@@ -1445,7 +1451,9 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction =
                    List.fold_left
                     (fun res a ->
                       if not (get_mark a) then
-                       (ToKeep (in_c,output_relation,output_direction))::res
+			List.map (fun output_direction ->
+			 (ToKeep (in_c,output_relation,output_direction)))
+			 output_directions @ res
                       else
                        let err =
                         match output_relation with
@@ -1461,7 +1469,9 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction =
                          let mor =
                           ACFunction{f_args=List.rev f_args_rev;f_output=typ} in
                          let func = beta_expand c c_args_rev in
-                          (MApp (func,mor,a,output_direction))::res
+			 List.map (fun output_direction ->
+                          (MApp (func,mor,a,output_direction)))
+			  output_directions @ res
                     ) [] a'
               | (he::tl) as a->
                  let typnf = Reduction.whd_betadeltaiota env typ in
@@ -1472,8 +1482,7 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction =
                   | Prod (name,s,t) ->
                      let env' = push_rel (name,None,s) env in
                      let he =
-                      (aux (Leibniz (Some s)) Left2Right he) @
-                      (aux (Leibniz (Some s)) Right2Left he) in
+                      (aux (Leibniz (Some s)) [Left2Right;Right2Left] he) in
                      if he = [] then []
                      else
                       let he0 = List.hd he in
@@ -1515,41 +1524,48 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction =
       | Prod (_, c1, c2) -> 
           if (dependent (mkRel 1) c2)
           then
-           errorlabstrm "Setoid_replace"
-            (str "Cannot rewrite in the type of a variable bound " ++
-             str "in a dependent product.")
+            if (occur_term t c2)
+	    then errorlabstrm "Setoid_replace"
+              (str "Cannot rewrite in the type of a variable bound " ++
+		  str "in a dependent product.")
+	    else
+	      List.map (fun output_direction ->
+	       ToKeep (in_c,output_relation,output_direction)) 
+	       output_directions
           else 
-           let typeofc1 = Tacmach.pf_type_of gl c1 in
-            if not (Tacmach.pf_conv_x gl typeofc1 mkProp) then
-             (* to avoid this error we should introduce an impl relation
-                whose first argument is Type instead of Prop. However,
-                the type of the new impl would be Type -> Prop -> Prop
-                that is no longer a Relation_Definitions.relation. Thus
-                the Coq part of the tactic should be heavily modified. *)
-             errorlabstrm "Setoid_replace"
-              (str "Rewriting in a product A -> B is possible only when A " ++
-               str "is a proposition (i.e. A is of type Prop). The type " ++
-               pr_lconstr c1 ++ str " has type " ++ pr_lconstr typeofc1 ++
-               str " that is not convertible to Prop.")
-            else
-             aux output_relation output_direction
-              (mkApp ((Lazy.force coq_impl),
-                [| c1 ; subst1 (mkRel 1 (*dummy*)) c2 |]))
+            let typeofc1 = Tacmach.pf_type_of gl c1 in
+              if not (Tacmach.pf_conv_x gl typeofc1 mkProp) then
+		(* to avoid this error we should introduce an impl relation
+                   whose first argument is Type instead of Prop. However,
+                   the type of the new impl would be Type -> Prop -> Prop
+                   that is no longer a Relation_Definitions.relation. Thus
+                   the Coq part of the tactic should be heavily modified. *)
+		errorlabstrm "Setoid_replace"
+		  (str "Rewriting in a product A -> B is possible only when A " ++
+		      str "is a proposition (i.e. A is of type Prop). The type " ++
+		      pr_lconstr c1 ++ str " has type " ++ pr_lconstr typeofc1 ++
+		      str " that is not convertible to Prop.")
+              else
+		aux output_relation output_directions
+		  (mkApp ((Lazy.force coq_impl),
+			 [| c1 ; subst1 (mkRel 1 (*dummy*)) c2 |]))
       | _ ->
-        if occur_term t in_c then
-         errorlabstrm "Setoid_replace"
-          (str "Trying to replace " ++ pr_lconstr t ++ str " in " ++ pr_lconstr in_c ++
-           str " that is not an applicative context.")
-        else
-         [ToKeep (in_c,output_relation,output_direction)]
+          if occur_term t in_c then
+            errorlabstrm "Setoid_replace"
+              (str "Trying to replace " ++ pr_lconstr t ++ str " in " ++ pr_lconstr in_c ++
+		  str " that is not an applicative context.")
+          else
+	    List.map (fun output_direction ->
+             ToKeep (in_c,output_relation,output_direction))
+	      output_directions
  in
   let aux2 output_relation output_direction =
    List.map
     (fun res -> output_relation,output_direction,res)
-     (aux output_relation output_direction in_c) in
+     (aux output_relation [output_direction] in_c) in
   let res =
    (aux2 (Lazy.force coq_iff_relation) Right2Left) @
-   (* This is the case of a proposition of signature A ++> iff or B --> iff *)
+   (* [Left2Right] is the case of a prop of signature A ++> iff or B --> iff *)
    (aux2 (Lazy.force coq_iff_relation) Left2Right) @
    (aux2 (Lazy.force coq_impl_relation) Right2Left) in
   let res = elim_duplicates gl (function (_,_,t) -> t) res in
@@ -1849,8 +1865,27 @@ let general_s_rewrite_in id lft2rgt c ~new_goals gl =
   else 
     relation_rewrite_in id c2 c1 (Right2Left,eqclause) ~new_goals gl
 
-let setoid_replace relation c1 c2 ~new_goals gl =
- try
+
+(* 
+   [general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_goals ]
+   common part of [setoid_replace] and [setoid_replace_in]  (distinction is done using rewrite_tac). 
+
+   Algorith sketch: 
+   1- find the (setoid) relation [rel] between [c1] and [c2] using [relation]
+   2- assert [H:rel c2 c1] 
+   3- replace [c1] with [c2] using [rewrite_tac] (should be [general_s_rewrite] if we want to replace in the 
+      goal, and [general_s_rewrite_in id] if we want to replace in the hypothesis [id]). Possibly generate
+      new_goals if asked (cf general_s_rewrite)
+   4- if [try_prove_eq_tac_opt] is [Some tac] try to complete [rel c2 c1] using tac and do nothing if 
+      [try_prove_eq_tac_opt] is [None]
+*)
+let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_goals gl =
+  let try_prove_eq_tac = 
+    match try_prove_eq_tac_opt with 
+      | None -> Tacticals.tclIDTAC
+      | Some tac ->  Tacticals.tclTRY (Tacticals.tclCOMPLETE tac )
+  in 
+  try
   let relation =
    match relation with
       Some rel ->
@@ -1873,23 +1908,29 @@ let setoid_replace relation c1 c2 ~new_goals gl =
     tclTHENS (assert_tac false Anonymous eq)
       [onLastHyp (fun id ->
         tclTHEN
-          (general_s_rewrite dir (mkVar id) ~new_goals)
+          (rewrite_tac dir (mkVar id) ~new_goals)
           (clear [id]));
-       Tacticals.tclIDTAC]
+       try_prove_eq_tac]
    in
     tclORELSE
      (replace true eq_left_to_right) (replace false eq_right_to_left) gl
  with
-  Optimize -> (!replace c1 c2) gl
+  Optimize -> (* (!replace tac_opt c1 c2) gl *)
+    let eq =  mkApp (Lazy.force  coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in 
+    tclTHENS (assert_tac false Anonymous eq)
+      [onLastHyp (fun id ->
+		    tclTHEN
+		      (rewrite_tac false (mkVar id) ~new_goals)
+		      (clear [id]));
+       try_prove_eq_tac] gl
+      
+
 
-let setoid_replace_in id relation c1 c2 ~new_goals gl =
- let hyp = pf_type_of gl (mkVar id) in
- let new_hyp = Termops.replace_term c1 c2 hyp in
- cut_replacing id new_hyp
-   (fun exact -> tclTHENLASTn
-     (setoid_replace relation c2 c1 ~new_goals)
-     [| exact; tclIDTAC |]) gl
 
+let setoid_replace = general_setoid_replace general_s_rewrite
+let setoid_replace_in  tac_opt id relation c1 c2 ~new_goals gl = 
+  general_setoid_replace (general_s_rewrite_in id)  tac_opt relation c1 c2 ~new_goals gl
+ 
 (* [setoid_]{reflexivity,symmetry,transitivity} tactics *)
 
 let setoid_reflexivity gl =
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index 750addcc..eb71f68e 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 8779 2006-05-02 20:59:21Z letouzey $ i*)
+(*i $Id: setoid_replace.mli 9073 2006-08-22 08:54:29Z jforest $ i*)
 
 open Term
 open Proof_type
@@ -39,7 +39,7 @@ type morphism_signature = (bool option * constr_expr) list * constr_expr
 
 val pr_morphism_signature : morphism_signature -> Pp.std_ppcmds
 
-val register_replace : (constr -> constr -> tactic) -> unit
+val register_replace : (tactic option -> constr -> constr -> tactic) -> unit
 val register_general_rewrite : (bool -> constr -> tactic) -> unit
 
 val print_setoids : unit -> unit
@@ -52,8 +52,9 @@ val default_morphism :
   ?filter:(constr morphism -> bool) -> constr -> relation morphism
 
 val setoid_replace :
- constr option -> constr -> constr -> new_goals:constr list -> tactic
+  tactic option -> constr option -> constr -> constr -> new_goals:constr list -> tactic
 val setoid_replace_in :
+  tactic option -> 
  identifier -> constr option -> constr -> constr -> new_goals:constr list ->
   tactic
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 114968c8..1e8c55ef 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacinterp.ml 8991 2006-06-27 11:59:50Z herbelin $ *)
+(* $Id: tacinterp.ml 9302 2006-10-27 21:21:17Z barras $ *)
 
 open Constrintern
 open Closure
@@ -48,6 +48,12 @@ open Pretyping
 open Pretyping.Default
 open Pcoq
 
+let safe_msgnl s =
+    try msgnl s with e -> 
+      msgnl 
+	(str "bug in the debugger : " ++
+         str "an exception is raised while printing debug information")
+
 let error_syntactic_metavariables_not_allowed loc =
   user_err_loc 
     (loc,"out_ident",
@@ -75,6 +81,7 @@ type value =
                         (* later, as in "tac" in "Intro H; tac" *)
   | VConstr of constr   (* includes idents known to be bound and references *)
   | VConstr_context of constr
+  | VList of value list
   | VRec of value ref
 
 let locate_tactic_call loc = function
@@ -112,13 +119,16 @@ let constr_of_VConstr_context = function
     errorlabstrm "constr_of_VConstr_context" (str "not a context variable")
 
 (* Displays a value *)
-let pr_value env = function
+let rec pr_value env = function
   | VVoid -> str "()"
   | VInteger n -> int n
   | VIntroPattern ipat -> pr_intro_pattern ipat
   | VConstr c | VConstr_context c ->
       (match env with Some env -> pr_lconstr_env env c | _ -> str "a term")
   | (VTactic _ | VRTactic _ | VFun _ | VRec _) -> str "a tactic"
+  | VList [] -> str "an empty list"
+  | VList (a::_) ->
+      str "a list (first element is " ++ pr_value env a ++ str")"
 
 (* Transforms a named_context into a (string * constr) list *)
 let make_hyps = List.map (fun (id,_,typ) -> (id, typ))
@@ -213,7 +223,7 @@ let _ =
       (fun (s,t) -> add_primitive_tactic s t)
       [ "idtac",TacId [];
         "fail", TacFail(ArgArg 0,[]);
-        "fresh", TacArg(TacFreshId None)
+        "fresh", TacArg(TacFreshId [])
       ]
  
 let lookup_atomic id = Idmap.find id !atomic_mactab
@@ -238,6 +248,34 @@ let _ =
       Summary.survive_module = false;
       Summary.survive_section   = false }
 
+(* Tactics table (TacExtend). *)
+
+let tac_tab = Hashtbl.create 17
+
+let add_tactic s t =
+  if Hashtbl.mem tac_tab s then
+    errorlabstrm ("Refiner.add_tactic: ") 
+      (str ("Cannot redeclare tactic "^s));
+  Hashtbl.add tac_tab s t
+
+let overwriting_add_tactic s t =
+  if Hashtbl.mem tac_tab s then begin
+    Hashtbl.remove tac_tab s;
+    warning ("Overwriting definition of tactic "^s)
+  end;
+  Hashtbl.add tac_tab s t
+
+let lookup_tactic s =
+  try 
+    Hashtbl.find tac_tab s
+  with Not_found -> 
+    errorlabstrm "Refiner.lookup_tactic"
+      (str"The tactic " ++ str s ++ str" is not installed")
+(*
+let vernac_tactic (s,args) =
+  let tacfun = lookup_tactic s args in
+  abstract_extended_tactic s args tacfun
+*)
 (* Interpretation of extra generic arguments *)
 type glob_sign = {
   ltacvars : identifier list * identifier list;
@@ -331,9 +369,9 @@ let intern_hyp ist (loc,id as locid) =
 
 let intern_hyp_or_metaid ist id = intern_hyp ist (skip_metaid id)
 
-let intern_int_or_var ist = function
+let intern_or_var ist = function
   | ArgVar locid -> ArgVar (intern_hyp ist locid)
-  | ArgArg n as x -> x
+  | ArgArg _ as x -> x
 
 let intern_inductive ist = function
   | Ident (loc,id) when find_var id ist -> ArgVar (loc,id)
@@ -495,7 +533,7 @@ let intern_inversion_strength lf ist = function
 
 (* Interprets an hypothesis name *)
 let intern_hyp_location ist ((occs,id),hl) =
-  ((List.map (intern_int_or_var ist) occs,intern_hyp ist (skip_metaid id)), hl)
+  ((List.map (intern_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,[])
@@ -527,7 +565,7 @@ let internalise_tacarg ch = G_xml.parse_tactic_arg ch
 let extern_tacarg ch env sigma = function
   | VConstr c -> !print_xml_term ch env sigma c
   | VTactic _ | VRTactic _ | VFun _ | VVoid | VInteger _ | VConstr_context _
-  | VIntroPattern _  | VRec _ ->
+  | VIntroPattern _  | VRec _ | VList _ ->
       error "Only externing of terms is implemented"
 
 let extern_request ch req gl la =
@@ -625,13 +663,13 @@ 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_map (intern_int_or_var ist) n,
+      TacAuto (option_map (intern_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_map (intern_int_or_var ist) n,p)
+  | TacDAuto (n,p) -> TacDAuto (option_map (intern_or_var ist) n,p)
 
   (* Derived basic tactics *)
   | TacSimpleInduction h ->
@@ -676,7 +714,8 @@ let rec intern_atomic lf ist x =
       TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl)
   | TacChange (occl,c,cl) ->
       TacChange (option_map (intern_constr_occurrence ist) occl,
-        intern_constr ist c, clause_app (intern_hyp_location ist) cl)
+        (if occl = None then intern_type ist c else intern_constr ist c),
+	clause_app (intern_hyp_location ist) cl)
 
   (* Equivalence relations *)
   | TacReflexivity -> TacReflexivity
@@ -728,7 +767,7 @@ and intern_tactic_seq ist = function
       ist.ltacvars, TacMatch (lz,intern_tactic ist c,intern_match_rule ist lmr)
   | TacId l -> ist.ltacvars, TacId (intern_message ist l)
   | TacFail (n,l) -> 
-      ist.ltacvars, TacFail (intern_int_or_var ist n,intern_message ist l)
+      ist.ltacvars, TacFail (intern_or_var ist n,intern_message ist l)
   | TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac)
   | TacAbstract (tac,s) -> ist.ltacvars, TacAbstract (intern_tactic ist tac,s)
   | TacThen (t1,t2) ->
@@ -741,7 +780,7 @@ and intern_tactic_seq ist = function
       lfun',
       TacThens (t, List.map (intern_tactic { ist with ltacvars = lfun' }) tl)
   | TacDo (n,tac) -> 
-      ist.ltacvars, TacDo (intern_int_or_var ist n,intern_tactic ist tac)
+      ist.ltacvars, TacDo (intern_or_var ist n,intern_tactic ist tac)
   | TacTry tac -> ist.ltacvars, TacTry (intern_tactic ist tac)
   | TacInfo tac -> ist.ltacvars, TacInfo (intern_tactic ist tac)
   | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_tactic ist tac)
@@ -776,7 +815,7 @@ and intern_tacarg strict ist = function
         List.map (intern_tacarg !strict_check ist) l)
   | TacExternal (loc,com,req,la) -> 
       TacExternal (loc,com,req,List.map (intern_tacarg !strict_check ist) la)
-  | TacFreshId _ as x -> x
+  | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x)
   | Tacexp t -> Tacexp (intern_tactic ist t)
   | TacDynamic(loc,t) as x ->
       (match tag t with
@@ -803,7 +842,7 @@ and intern_genarg ist x =
   | IntArgType -> in_gen globwit_int (out_gen rawwit_int x)
   | IntOrVarArgType ->
       in_gen globwit_int_or_var
-        (intern_int_or_var ist (out_gen rawwit_int_or_var x))
+        (intern_or_var ist (out_gen rawwit_int_or_var x))
   | StringArgType ->
       in_gen globwit_string (out_gen rawwit_string x)
   | PreIdentArgType ->
@@ -1045,6 +1084,19 @@ let interp_int_or_var ist = function
   | ArgVar locid -> interp_int ist locid
   | ArgArg n -> n
 
+let int_or_var_list_of_VList = function
+  | VList l -> List.map (fun n -> ArgArg (coerce_to_int n)) l
+  | _ -> raise Not_found
+
+let interp_int_or_var_as_list ist = function
+  | ArgVar (_,id as locid) -> 
+      (try int_or_var_list_of_VList (List.assoc id ist.lfun)
+       with Not_found | CannotCoerceTo _ -> [ArgArg (interp_int ist locid)])
+  | ArgArg n as x -> [x]
+
+let interp_int_or_var_list ist l =
+  List.flatten (List.map (interp_int_or_var_as_list ist) l)
+
 let constr_of_value env = function
   | VConstr csr -> csr
   | VIntroPattern (IntroIdentifier id) -> constr_of_id env id
@@ -1065,6 +1117,17 @@ let interp_hyp ist gl (loc,id as locid) =
   if is_variable env id then id
   else user_err_loc (loc,"eval_variable",pr_id id ++ str " not found")
 
+let hyp_list_of_VList env = function
+  | VList l -> List.map (coerce_to_hyp env) l
+  | _ -> raise Not_found
+
+let interp_hyp_list_as_list ist gl (loc,id as x) =
+  try hyp_list_of_VList (pf_env gl) (List.assoc id ist.lfun)
+  with Not_found | CannotCoerceTo _ -> [interp_hyp ist gl x]
+
+let interp_hyp_list ist gl l =
+  List.flatten (List.map (interp_hyp_list_as_list ist gl) l)
+
 let interp_clause_pattern ist gl (l,occl) =
   let rec check acc = function
     | (hyp,l) :: rest ->
@@ -1126,8 +1189,7 @@ let interp_evaluable ist env = function
 
 (* Interprets an hypothesis name *)
 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)
+  ((interp_int_or_var_list ist occs,interp_hyp ist gl id),hl)
 
 let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } =
   { onhyps=option_map(List.map (interp_hyp_location ist gl)) ol;
@@ -1157,11 +1219,25 @@ let rec intropattern_ids = function
       List.flatten (List.map intropattern_ids (List.flatten ll))
   | IntroWildcard | IntroAnonymous -> []
 
-let rec extract_ids = function
-  | (id,VIntroPattern ipat)::tl -> intropattern_ids ipat @ extract_ids tl
-  | _::tl -> extract_ids tl
+let rec extract_ids ids = function
+  | (id,VIntroPattern ipat)::tl when not (List.mem id ids) ->
+      intropattern_ids ipat @ extract_ids ids tl
+  | _::tl -> extract_ids ids tl
   | [] -> []
 
+let default_fresh_id = id_of_string "H"
+
+let interp_fresh_id ist gl l =
+  let ids = map_succeed (function ArgVar(_,id) -> id | _ -> failwith "") l in
+  let avoid = extract_ids ids ist.lfun in
+  let id = 
+    if l = [] then default_fresh_id 
+    else
+      id_of_string (String.concat "" (List.map (function
+	| ArgArg s -> s
+	| ArgVar (_,id) -> string_of_id (interp_ident ist gl id)) l)) in 
+  Tactics.fresh_id avoid id gl
+
 (* To retype a list of key*constr with undefined key *)
 let retype_list sigma env lst =
   List.fold_right (fun (x,csr) a ->
@@ -1210,7 +1286,7 @@ let solve_remaining_evars env initial_sigma evars c =
 	      Pretype_errors.error_unsolvable_implicit loc env sigma src)
       | _ -> map_constr proc_rec c      
   in
-  map_constr proc_rec c
+  proc_rec c
 
 let interp_gen kind ist sigma env (c,ce) =
   let (ltacvars,unbndltacvars) = constr_list ist env in
@@ -1254,20 +1330,33 @@ let pf_interp_open_constr casted ist gl cc =
 let pf_interp_constr ist gl =
   interp_constr ist (project gl) (pf_env gl)
 
+let constr_list_of_VList env = function
+  | VList l -> List.map (constr_of_value env) l
+  | _ -> raise Not_found
+      
+let pf_interp_constr_list_as_list ist gl (c,_ as x) =
+  match c with
+    | RVar (_,id) ->
+        (try constr_list_of_VList (pf_env gl) (List.assoc id ist.lfun)
+        with Not_found -> [interp_constr ist (project gl) (pf_env gl) x])
+    | _ -> [interp_constr ist (project gl) (pf_env gl) x]
+
+let pf_interp_constr_list ist gl l =
+  List.flatten (List.map (pf_interp_constr_list_as_list ist gl) l)
+
 (* Interprets a type expression *)
 let pf_interp_type ist gl =
   interp_type ist (project gl) (pf_env gl)
 
 (* Interprets a reduction expression *)
 let interp_unfold ist env (l,qid) =
-  (l,interp_evaluable ist env qid)
+  (interp_int_or_var_list ist l,interp_evaluable ist env 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) = 
-  (List.map (fun n -> ArgArg (interp_int_or_var ist n)) l,
-   interp_constr ist sigma env c)
+  (interp_int_or_var_list ist l, interp_constr ist sigma env c)
 
 let pf_interp_pattern ist gl = interp_pattern ist (project gl) (pf_env gl)
 
@@ -1296,11 +1385,39 @@ let interp_may_eval f ist gl = function
 	    user_err_loc (loc, "interp_may_eval",
 	    str "Unbound context identifier" ++ pr_id s))
   | ConstrTypeOf c -> pf_type_of gl (f ist gl c)
-  | ConstrTerm c -> f ist gl c
+  | ConstrTerm c -> 
+     try 
+	f ist gl c
+     with e -> 
+	begin 
+	  match ist.debug with 
+	    DebugOn lev -> 
+	    safe_msgnl (str "Level " ++ int lev ++
+                          str ": interpretation of term " ++ 
+			   Printer.pr_rawconstr_env (pf_env gl) (fst c) ++
+			   str " raised an exception" ++
+			   fnl() ++
+			   !Tactic_debug.explain_logic_error_no_anomaly e)
+	| _ -> ()
+     end;
+     raise e  
 
 (* Interprets a constr expression possibly to first evaluate *)
 let interp_constr_may_eval ist gl c =
-  let csr = interp_may_eval pf_interp_constr ist gl c in
+  let csr = 
+    try
+      interp_may_eval pf_interp_constr ist gl c
+    with e -> 
+      begin match ist.debug with
+	  DebugOn lev -> 
+	    safe_msgnl (str "Level " ++ int lev ++
+                           str ": evaluation of term raised an exception" ++
+			   fnl() ++
+			   !Tactic_debug.explain_logic_error_no_anomaly e)
+	| _ -> ()
+      end;
+      raise e
+  in
   begin
     db_constr ist.debug (pf_env gl) csr;
     csr
@@ -1312,6 +1429,7 @@ let message_of_value = function
   | VIntroPattern ipat -> pr_intro_pattern ipat
   | VConstr_context c | VConstr c -> pr_constr c
   | VRec _ | VTactic _ | VRTactic _ | VFun _ -> str "<tactic>"
+  | VList _ -> str "<list>"
 
 let rec interp_message ist = function
   | [] -> mt()
@@ -1380,12 +1498,16 @@ let interp_binding ist gl (loc,b,c) =
 
 let interp_bindings ist gl = function
 | NoBindings -> NoBindings
-| ImplicitBindings l -> ImplicitBindings (List.map (pf_interp_constr ist gl) l)
+| ImplicitBindings l -> ImplicitBindings (pf_interp_constr_list ist gl l)
 | ExplicitBindings l -> ExplicitBindings (List.map (interp_binding ist gl) l)
 
 let interp_constr_with_bindings ist gl (c,bl) =
   (pf_interp_constr ist gl c, interp_bindings ist gl bl)
 
+let mk_constr_value ist gl c = VConstr (pf_interp_constr ist gl c)
+let mk_hyp_value ist gl c = VConstr (mkVar (interp_hyp ist gl c))
+let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c)
+
 (* Interprets an l-tac expression into a value *)
 let rec val_interp ist gl (tac:glob_tactic_expr) =
 
@@ -1453,9 +1575,8 @@ and interp_tacarg ist gl = function
       interp_app ist gl fv largs loc
   | TacExternal (loc,com,req,la) ->
       interp_external loc ist gl com req (List.map (interp_tacarg ist gl) la)
-  | TacFreshId idopt -> 
-      let s = match idopt with None -> "H" | Some s -> s in
-      let id = Tactics.fresh_id (extract_ids ist.lfun) (id_of_string s) gl in
+  | TacFreshId l -> 
+      let id = interp_fresh_id ist gl l in
       VIntroPattern (IntroIdentifier id)
   | Tacexp t -> val_interp ist gl t
   | TacDynamic(_,t) ->
@@ -1481,7 +1602,31 @@ and interp_app ist gl fv largs loc =
     | VFun(olfun,var,body) ->
       let (newlfun,lvar,lval)=head_with_value (var,largs) in
       if lvar=[] then
-	let v = val_interp { ist with lfun=newlfun@olfun } gl body in
+	let v = 
+          let res = 
+	    try
+	      val_interp { ist with lfun=newlfun@olfun } gl body
+	    with e ->
+	      begin match ist.debug with
+		  DebugOn lev -> 
+		    safe_msgnl 
+		      (str "Level " ++ int lev ++ 
+			  str ": evaluation raises an exception" ++
+                          fnl() ++
+			  !Tactic_debug.explain_logic_error_no_anomaly e)
+		| _ -> ()
+	      end;
+	      raise e
+	  in
+	    (match ist.debug with
+		DebugOn lev -> 
+		  safe_msgnl (str "Level " ++ int lev ++ 
+				 str ": evaluation returns" ++ fnl() ++
+				 pr_value (Some (pf_env gl)) res)
+	      | _ -> ());
+	    res
+	in
+
         if lval=[] then locate_tactic_call loc v
 	else interp_app ist gl v lval loc
       else
@@ -1559,52 +1704,52 @@ and interp_match_context ist g lz lr lmr =
   let rec apply_goal_sub ist env goal nocc (id,c) csr mt mhyps hyps =
     let (lgoal,ctxt) = match_subterm nocc c csr in
     let lctxt = give_context ctxt id in
-    try apply_hyps_context ist env lz goal mt lctxt lgoal mhyps hyps
-    with e when is_match_catchable e ->
-      apply_goal_sub ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in
+      try apply_hyps_context ist env lz goal mt lctxt lgoal mhyps hyps
+      with e when is_match_catchable e ->
+	apply_goal_sub ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in
   let rec apply_match_context ist env goal nrs lex lpt = 
     begin
-    if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex);
-    match lpt with
-    | (All t)::tl ->
-      begin
-        db_mc_pattern_success ist.debug;
-        try eval_with_fail ist lz goal t
-        with e when is_match_catchable e ->
-          apply_match_context ist env goal (nrs+1) (List.tl lex) tl
-      end
-    | (Pat (mhyps,mgoal,mt))::tl ->
-      let hyps = make_hyps (pf_hyps goal) in
-      let hyps = if lr then List.rev hyps else hyps in
-      let mhyps = List.rev mhyps (* Sens naturel *) in
-      let concl = pf_concl goal in
-      (match mgoal with
-      |	Term mg ->
-        (try
-           let lgoal = matches mg concl in
-           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
-            | PatternMatchingFailure -> db_matching_failure ist.debug
-            | Eval_fail s -> db_eval_failure ist.debug s
-            | _ -> db_logic_failure ist.debug e);
-          apply_match_context ist env goal (nrs+1) (List.tl lex) tl)
-      |	Subterm (id,mg) ->
-        (try apply_goal_sub ist env goal 0 (id,mg) concl mt mhyps hyps
-        with
-        | PatternMatchingFailure ->
-           apply_match_context ist env goal (nrs+1) (List.tl lex) tl))
-    | _ ->
-      errorlabstrm "Tacinterp.apply_match_context"
-        (v 0 (str "No matching clauses for match goal" ++
-        (if ist.debug=DebugOff then
-           fnl() ++ str "(use \"Debug On\" for more info)"
-         else mt())))
+      if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex);
+      match lpt with
+	| (All t)::tl ->
+	    begin
+              db_mc_pattern_success ist.debug;
+              try eval_with_fail ist lz goal t
+              with e when is_match_catchable e ->
+		apply_match_context ist env goal (nrs+1) (List.tl lex) tl
+	    end
+	| (Pat (mhyps,mgoal,mt))::tl ->
+	    let hyps = make_hyps (pf_hyps goal) in
+	    let hyps = if lr then List.rev hyps else hyps in
+	    let mhyps = List.rev mhyps (* Sens naturel *) in
+	    let concl = pf_concl goal in
+	      (match mgoal with
+		 | Term mg ->
+		     (try
+			let lgoal = matches mg concl in
+			  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
+			   | PatternMatchingFailure -> db_matching_failure ist.debug
+			   | Eval_fail s -> db_eval_failure ist.debug s
+			   | _ -> db_logic_failure ist.debug e);
+			apply_match_context ist env goal (nrs+1) (List.tl lex) tl)
+		 | Subterm (id,mg) ->
+		     (try apply_goal_sub ist env goal 0 (id,mg) concl mt mhyps hyps
+		      with
+			| PatternMatchingFailure ->
+			    apply_match_context ist env goal (nrs+1) (List.tl lex) tl))
+	| _ ->
+	    errorlabstrm "Tacinterp.apply_match_context"
+              (v 0 (str "No matching clauses for match goal" ++
+		      (if ist.debug=DebugOff then
+			 fnl() ++ str "(use \"Debug On\" for more info)"
+		       else mt())))
     end in
   let env = pf_env g in
-  apply_match_context ist env g 0 lmr
-    (read_match_rule (fst (constr_list ist env)) lmr)
+    apply_match_context ist env g 0 lmr
+      (read_match_rule (fst (constr_list ist env)) lmr)
 
 (* Tries to match the hypotheses in a Match Context *)
 and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
@@ -1679,6 +1824,8 @@ and interp_genarg ist gl x =
   | BindingsArgType ->
       in_gen wit_bindings
         (interp_bindings ist gl (out_gen globwit_bindings x))
+  | List0ArgType ConstrArgType -> interp_genarg_constr_list0 ist gl x
+  | List1ArgType ConstrArgType -> interp_genarg_constr_list1 ist gl x
   | List0ArgType _ -> app_list0 (interp_genarg ist gl) x
   | List1ArgType _ -> app_list1 (interp_genarg ist gl) x
   | OptArgType _ -> app_opt (interp_genarg ist gl) x
@@ -1691,6 +1838,16 @@ and interp_genarg ist gl x =
       | None -> 
           lookup_interp_genarg s ist gl x
 
+and interp_genarg_constr_list0 ist gl x =
+  let lc = out_gen (wit_list0 globwit_constr) x in
+  let lc = pf_interp_constr_list ist gl lc in
+  in_gen (wit_list0 wit_constr) lc
+
+and interp_genarg_constr_list1 ist gl x =
+  let lc = out_gen (wit_list1 globwit_constr) x in
+  let lc = pf_interp_constr_list ist gl lc in
+  in_gen (wit_list1 wit_constr) lc
+
 (* Interprets the Match expressions *)
 and interp_match ist g lz constr lmr =
   let rec apply_match_subterm ist nocc (id,c) csr mt =
@@ -1706,26 +1863,115 @@ and interp_match ist g lz constr lmr =
         (try eval_with_fail ist lz g t
          with e when is_match_catchable e -> apply_match ist csr [])
     | (Pat ([],Term c,mt))::tl ->
-        (try
-	  let lm = matches c csr in
-	  let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
-          eval_with_fail { ist with lfun=lm@ist.lfun } lz g mt
-         with e when is_match_catchable e -> apply_match ist csr tl)
+        (try let lm = 
+              (try matches c csr with 
+                e -> 
+                  (match ist.debug with
+                    DebugOn lev ->
+                      safe_msgnl (str "Level " ++ int lev ++
+                             str ": matching with pattern" ++ fnl() ++
+                         Printer.pr_constr_pattern_env (pf_env g) c ++ fnl() ++
+                         str "raised the exception" ++ fnl() ++
+                         !Tactic_debug.explain_logic_error_no_anomaly e)
+                  | _ -> ()); raise e) in
+            (try let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
+               eval_with_fail { ist with lfun=lm@ist.lfun } lz g mt
+            with e ->
+               (match ist.debug with
+                  DebugOn lev -> 
+                    safe_msgnl (str "rule body for pattern" ++ fnl() ++
+                    Printer.pr_constr_pattern_env (pf_env g) c ++ fnl() ++
+                    str "raised the exception" ++ fnl() ++
+                    !Tactic_debug.explain_logic_error_no_anomaly e)
+                | _ -> ()); raise e)
+         with e when is_match_catchable e ->
+            (match ist.debug with
+               DebugOn lev ->
+                 safe_msgnl (str "Level " ++ int lev ++ 
+                       str ":switching to the next rule");
+             | DebugOff -> ());
+            apply_match ist csr tl)
+
     | (Pat ([],Subterm (id,c),mt))::tl ->
         (try apply_match_subterm ist 0 (id,c) csr mt
          with PatternMatchingFailure -> apply_match ist csr tl)
     | _ ->
       errorlabstrm "Tacinterp.apply_match" (str
         "No matching clauses for match") in
-  let csr = interp_ltac_constr ist g constr in
+  let csr = 
+      try interp_ltac_constr ist g constr with
+        e -> (match ist.debug with
+               DebugOn lev ->
+               safe_msgnl (str "Level " ++ int lev ++ 
+                      str ": evaluation of the matched expression raised " ++
+                      str "the exception" ++ fnl() ++
+                      !Tactic_debug.explain_logic_error e)
+             | _ -> ()); raise e in
   let ilr = read_match_rule (fst (constr_list ist (pf_env g))) lmr in
-  apply_match ist csr ilr
+  let res = 
+     try apply_match ist csr ilr with
+       e -> 
+           begin match ist.debug with
+             DebugOn lev ->
+                safe_msgnl (str "Level " ++ int lev ++ 
+                        str ": match expression failed with error" ++ fnl() ++
+                    !Tactic_debug.explain_logic_error e)
+           | _ -> ()
+           end;
+           raise e in
+     (if ist.debug <> DebugOff then
+     safe_msgnl (str "match expression returns " ++
+            pr_value (Some (pf_env g)) res));
+     res
 
 (* Interprets tactic expressions : returns a "constr" *)
 and interp_ltac_constr ist gl e =
-  try constr_of_value (pf_env gl) (val_interp ist gl e)
+  let result = 
+  try (val_interp ist gl e) with Not_found -> 
+    begin match ist.debug with
+      DebugOn lev ->
+       safe_msgnl (str "Level " ++ int lev ++ 
+                   str ": evaluation failed for" ++ fnl() ++
+                       Pptactic.pr_glob_tactic (pf_env gl) e)
+    | _ -> ()
+    end;
+    raise Not_found in
+  try let cresult = constr_of_value (pf_env gl) result in
+    (if !debug <> DebugOff then 
+        safe_msgnl (Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++
+        str " has value " ++ fnl() ++ print_constr_env (pf_env gl) cresult);
+     cresult)
+        
   with Not_found ->
-    errorlabstrm "" (str "Must evaluate to a term")
+    errorlabstrm ""
+      (str "Must evaluate to a term" ++ fnl() ++ 
+	  str "offending expression: " ++ fnl() ++
+          Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++ str "this is a " ++
+          (match result with
+              VTactic _ -> str "VTactic"
+            | VRTactic _ -> str "VRTactic"
+            | VFun (il,ul,b) ->
+                (str "VFun with body " ++ fnl() ++
+                    Pptactic.pr_glob_tactic (pf_env gl) b ++ fnl() ++
+		    str "instantiated arguments " ++ fnl() ++
+                    List.fold_right 
+                    (fun p s ->
+                      let (i,v) = p in str (string_of_id i) ++ str ", " ++ s)
+                    il (str "") ++
+                    str "uninstantiated arguments " ++ fnl() ++
+                    List.fold_right
+                    (fun opt_id s ->
+                      (match opt_id with
+                          Some id -> str (string_of_id id)
+                        | None -> str "_") ++ str ", " ++ s)
+                    ul (str ""))
+            | VVoid -> str "VVoid"
+            | VInteger _ -> str "VInteger"
+            | VConstr _ -> str "VConstr"
+            | VIntroPattern _ -> str "VIntroPattern"
+            | VConstr_context _ -> str "VConstrr_context"
+            | VRec _ -> str "VRec"
+            | VList _ -> str "VList"))
 
 (* Interprets tactic expressions : returns a "tactic" *)
 and interp_tactic ist tac gl =
@@ -1767,7 +2013,7 @@ and interp_atomic ist gl = function
       abstract_tactic (TacAssert (t,ipat,c))
         (Tactics.forward (option_map (interp_tactic ist) t)
 	  (interp_intro_pattern ist gl ipat) c)
-  | TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl)
+  | TacGeneralize cl -> h_generalize (pf_interp_constr_list ist gl cl)
   | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
   | TacLetTac (na,c,clp) ->
       let clp = interp_clause ist gl clp in
@@ -1781,11 +2027,11 @@ and interp_atomic ist gl = function
 *)
   (* Automation tactics *)
   | TacTrivial (lems,l) -> 
-      Auto.h_trivial (List.map (pf_interp_constr ist gl) lems)
+      Auto.h_trivial (pf_interp_constr_list ist gl lems)
 	(option_map (List.map (interp_hint_base ist)) l)
   | TacAuto (n,lems,l) ->
       Auto.h_auto (option_map (interp_int_or_var ist) n)
-      (List.map (pf_interp_constr ist gl) lems)
+      (pf_interp_constr_list ist gl lems)
       (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)
@@ -1820,8 +2066,8 @@ and interp_atomic ist gl = function
   | TacLApply c -> h_lapply (pf_interp_constr ist gl c)
 
   (* Context management *)
-  | TacClear (b,l) -> h_clear b (List.map (interp_hyp ist gl) l)
-  | TacClearBody l -> h_clear_body (List.map (interp_hyp ist gl) l)
+  | TacClear (b,l) -> h_clear b (interp_hyp_list ist gl l)
+  | TacClearBody l -> h_clear_body (interp_hyp_list ist gl l)
   | TacMove (dep,id1,id2) ->
       h_move dep (interp_hyp ist gl id1) (interp_hyp ist gl id2)
   | TacRename (id1,id2) ->
@@ -1842,7 +2088,9 @@ and interp_atomic ist gl = function
       h_reduce (pf_interp_red_expr ist gl r) (interp_clause ist gl cl)
   | TacChange (occl,c,cl) ->
       h_change (option_map (pf_interp_pattern ist gl) occl)
-        (pf_interp_constr ist gl c) (interp_clause ist gl cl)
+        (if occl = None then pf_interp_type ist gl c 
+	 else pf_interp_constr ist gl c)
+        (interp_clause ist gl cl)
 
   (* Equivalence relations *)
   | TacReflexivity -> h_reflexivity
@@ -1861,21 +2109,25 @@ and interp_atomic ist gl = function
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
       Inv.inv_clause k 
         (interp_intro_pattern ist gl ids)
-        (List.map (interp_hyp ist gl) idl)
+        (interp_hyp_list ist gl idl)
         (interp_declared_or_quantified_hypothesis ist gl hyp)
   | TacInversion (InversionUsing (c,idl),hyp) ->
       Leminv.lemInv_clause (interp_declared_or_quantified_hypothesis ist gl hyp)
         (pf_interp_constr ist gl c)
-        (List.map (interp_hyp ist gl) idl)
+        (interp_hyp_list ist gl idl)
 
   (* For extensions *)
   | TacExtend (loc,opn,l) ->
-      fun gl -> vernac_tactic (opn,List.map (interp_genarg ist gl) l) gl
+      let tac = lookup_tactic opn in
+      fun gl ->
+        let args = List.map (interp_genarg ist gl) l in
+        abstract_extended_tactic opn args (tac args) gl
   | TacAlias (loc,_,l,(_,body)) -> fun gl ->
     let rec f x = match genarg_tag x with
-    | IntArgType -> VInteger (out_gen globwit_int x)
-    | IntOrVarArgType -> 
-	VInteger (interp_int_or_var ist (out_gen globwit_int_or_var x))
+    | IntArgType -> 
+        VInteger (out_gen globwit_int x)
+    | IntOrVarArgType ->
+        mk_int_or_var_value ist (out_gen globwit_int_or_var x)
     | PreIdentArgType ->
 	failwith "pre-identifiers cannot be bound"
     | IntroPatternArgType ->
@@ -1885,14 +2137,14 @@ and interp_atomic ist gl = function
         VIntroPattern 
 	  (IntroIdentifier (interp_ident ist gl (out_gen globwit_ident x)))
     | VarArgType ->
-	VConstr (mkVar (interp_hyp ist gl (out_gen globwit_var x)))
+        mk_hyp_value ist gl (out_gen globwit_var x)
     | RefArgType -> 
         VConstr (constr_of_global 
           (pf_interp_reference ist gl (out_gen globwit_ref x)))
-    | SortArgType ->
-	VConstr (mkSort (interp_sort (out_gen globwit_sort x)))
+    | SortArgType -> 
+        VConstr (mkSort (interp_sort (out_gen globwit_sort x)))
     | ConstrArgType ->
-        VConstr (pf_interp_constr ist gl (out_gen globwit_constr x))
+        mk_constr_value ist gl (out_gen globwit_constr x)
     | ConstrMayEvalArgType ->
 	VConstr
           (interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x))
@@ -1900,11 +2152,36 @@ and interp_atomic ist gl = function
           (* Special treatment of tactic arguments *)
 	val_interp ist gl 
           (out_gen (globwit_tactic (out_some (tactic_genarg_level s))) x)
+    | List0ArgType ConstrArgType -> 
+        let wit = wit_list0 globwit_constr in
+        VList (List.map (mk_constr_value ist gl) (out_gen wit x))
+    | List0ArgType VarArgType -> 
+        let wit = wit_list0 globwit_var in
+        VList (List.map (mk_hyp_value ist gl) (out_gen wit x))
+    | List0ArgType IntArgType -> 
+        let wit = wit_list0 globwit_int in
+        VList (List.map (fun x -> VInteger x) (out_gen wit x))
+    | List0ArgType IntOrVarArgType -> 
+        let wit = wit_list0 globwit_int_or_var in
+        VList (List.map (mk_int_or_var_value ist) (out_gen wit x))
+    | List1ArgType ConstrArgType -> 
+        let wit = wit_list1 globwit_constr in
+        VList (List.map (mk_constr_value ist gl) (out_gen wit x))
+    | List1ArgType VarArgType -> 
+        let wit = wit_list1 globwit_var in
+        VList (List.map (mk_hyp_value ist gl) (out_gen wit x))
+    | List1ArgType IntArgType -> 
+        let wit = wit_list1 globwit_int in
+        VList (List.map (fun x -> VInteger x) (out_gen wit x))
+    | List1ArgType IntOrVarArgType -> 
+        let wit = wit_list1 globwit_int_or_var in
+        VList (List.map (mk_int_or_var_value ist) (out_gen wit x))
     | StringArgType | BoolArgType
     | QuantHypArgType | RedExprArgType 
     | OpenConstrArgType _ | ConstrWithBindingsArgType 
     | ExtraArgType _ | BindingsArgType 
-    | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ 
+    | OptArgType _ | PairArgType _ 
+    | List0ArgType _ | List1ArgType _ 
 	-> error "This generic type is not supported in alias"
         
     in
@@ -1925,7 +2202,7 @@ let interp_tac_gen lfun debug t gl =
       ltacvars = (List.map fst lfun, []); ltacrecvars = [];
       gsigma = project gl; genv = pf_env gl } t) gl
 
-let eval_tactic t = interp_tactic { lfun=[]; debug=get_debug() } t
+let eval_tactic t gls = interp_tactic { lfun=[]; debug=get_debug() } t gls
 
 let interp t = interp_tac_gen [] (get_debug()) t
 
@@ -1941,7 +2218,8 @@ let hide_interp t ot gl =
   let t = eval_tactic te in
   match ot with 
   | None -> abstract_tactic_expr (TacArg (Tacexp te)) t gl
-  | Some t' -> abstract_tactic_expr (TacArg (Tacexp te)) (tclTHEN t t') gl
+  | Some t' ->
+      abstract_tactic_expr ~dflt:true (TacArg (Tacexp te)) (tclTHEN t t') gl
 
 (***************************************************************************)
 (* Substitution at module closing time *)
@@ -1973,7 +2251,7 @@ let subst_induction_arg subst = function
   | ElimOnIdent id as x -> x
 
 let subst_and_short_name f (c,n) =
-  assert (n=None); (* since tacdef are strictly globalized *)
+(*  assert (n=None); *)(* since tacdef are strictly globalized *)
   (f c,None)
 
 let subst_or_var f =  function
@@ -2170,9 +2448,11 @@ and subst_tacarg subst = function
       TacExternal (_loc,com,req,List.map (subst_tacarg subst) la)
   | (TacVoid | IntroPattern _ | Integer _ | TacFreshId _) as x -> x
   | Tacexp t -> Tacexp (subst_tactic subst t)
-  | TacDynamic(_,t) as x ->
+  | TacDynamic(the_loc,t) as x ->
       (match tag t with
-	| "tactic" | "value" | "constr" -> x
+	| "tactic" | "value" -> x
+        | "constr" -> 
+          TacDynamic(the_loc, constr_in (subst_mps subst (constr_out t)))
 	| s -> anomaly_loc (dloc, "Tacinterp.val_interp",
                  str "Unknown dynamic: <" ++ str s ++ str ">"))
 
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 7c0180a6..01e7750a 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacinterp.mli 8975 2006-06-23 08:52:53Z herbelin $ i*)
+(*i $Id: tacinterp.mli 9178 2006-09-26 11:18:22Z barras $ i*)
 
 (*i*)
 open Dyn
@@ -34,6 +34,7 @@ type value =
   | VIntroPattern of intro_pattern_expr
   | VConstr of constr
   | VConstr_context of constr
+  | VList of value list
   | VRec of value ref
 
 (* Signature for interpretation: val\_interp and interpretation functions *)
@@ -63,6 +64,14 @@ val add_tacdef :
   bool -> (identifier Util.located * raw_tactic_expr) list -> unit
 val add_primitive_tactic : string -> glob_tactic_expr -> unit
 
+(* Tactic extensions *)
+val add_tactic :
+  string -> (closed_generic_argument list -> tactic) -> unit
+val overwriting_add_tactic :
+  string -> (closed_generic_argument list -> tactic) -> unit
+val lookup_tactic :
+  string -> (closed_generic_argument list) -> tactic
+
 (* Adds an interpretation function for extra generic arguments *)
 type glob_sign = {
   ltacvars : identifier list * identifier list;
@@ -84,6 +93,9 @@ val interp_genarg :
 val intern_genarg :
   glob_sign -> raw_generic_argument -> glob_generic_argument
 
+val intern_tactic : 
+  glob_sign -> raw_tactic_expr -> glob_tactic_expr
+
 val intern_constr :
   glob_sign -> constr_expr -> rawconstr_and_expr
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index ff6ac41a..06289169 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacticals.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
+(* $Id: tacticals.ml 9211 2006-10-05 12:38:33Z letouzey $ *)
 
 open Pp
 open Util
@@ -68,6 +68,7 @@ let tclTHENTRY       = tclTHENTRY
 let tclIFTHENELSE    = tclIFTHENELSE
 let tclIFTHENSELSE   = tclIFTHENSELSE
 let tclIFTHENSVELSE   = tclIFTHENSVELSE
+let tclIFTHENTRYELSEMUST = tclIFTHENTRYELSEMUST
 
 let unTAC            = unTAC
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 7ceddc8b..458ab732 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacticals.mli 7909 2006-01-21 11:09:18Z herbelin $ i*)
+(*i $Id: tacticals.mli 9211 2006-10-05 12:38:33Z letouzey $ i*)
 
 (*i*)
 open Pp
@@ -64,7 +64,7 @@ val tclIFTHENELSE    : tactic -> tactic -> tactic -> tactic
 val tclIFTHENSELSE   : tactic -> tactic list -> tactic -> tactic
 val tclIFTHENSVELSE  : tactic -> tactic array -> tactic -> tactic
 
-
+val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
 
 val unTAC            : tactic -> goal sigma -> proof_tree sigma
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4eaf0259..f77814de 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactics.ml 8878 2006-05-30 16:44:25Z herbelin $ *)
+(* $Id: tactics.ml 9281 2006-10-26 07:52:31Z herbelin $ *)
 
 open Pp
 open Util
@@ -245,20 +245,22 @@ let unfold_constr = function
 (*         Introduction tactics            *)
 (*******************************************)
 
+let fresh_id_avoid avoid id =
+  next_global_ident_away true id avoid
+
 let fresh_id avoid id gl =
-  next_global_ident_away true id (avoid@(pf_ids_of_hyps gl))
+  fresh_id_avoid (avoid@(pf_ids_of_hyps gl)) id
 
 let id_of_name_with_default s = function
   | Anonymous -> id_of_string s
   | Name id   -> id
 
-let default_id gl = function
+let default_id env sigma = function
   | (name,None,t) ->
-      (match kind_of_term (pf_whd_betadeltaiota gl (pf_type_of gl t)) with
-	| Sort (Prop _) -> (id_of_name_with_default "H" name)
-	| Sort (Type _) -> (id_of_name_with_default "X" name)
-	| _                   -> anomaly "Wrong sort")
-  | (name,Some b,_) -> id_of_name_using_hdchar (pf_env gl) b name
+      (match Typing.sort_of env sigma t with
+	| Prop _ -> (id_of_name_with_default "H" name)
+	| Type _ -> (id_of_name_with_default "X" name))
+  | (name,Some b,_) -> id_of_name_using_hdchar env b name
 
 (* Non primitive introduction tactics are treated by central_intro
    There is possibly renaming, with possibly names to avoid and 
@@ -270,14 +272,32 @@ type intro_name_flag =
   | IntroMustBe of identifier
 
 let find_name decl gl = function
-  | IntroAvoid idl        -> 
-      let id = fresh_id idl (default_id gl decl) gl in id
+  | IntroAvoid idl -> 
+      (* this case must be compatible with [find_intro_names] below. *)
+      let id = fresh_id idl (default_id (pf_env gl) gl.sigma decl) gl in id
   | IntroBasedOn (id,idl) -> fresh_id idl id gl
   | IntroMustBe id        -> 
       let id' = fresh_id [] id gl in
       if id' <> id then error ((string_of_id id)^" is already used");
       id'
 
+(* Returns the names that would be created by intros, without doing
+   intros.  This function is supposed to be compatible with an
+   iteration of [find_name] above. As [default_id] checks the sort of
+   the type to build hyp names, we maintain an environment to be able
+   to type dependent hyps. *)
+let find_intro_names ctxt gl = 
+  let _, res = List.fold_right 
+    (fun decl acc -> 
+      let wantedname,x,typdecl = decl in
+      let env,idl = acc in
+      let name = fresh_id idl (default_id env gl.sigma decl) gl in
+      let newenv = push_rel (wantedname,x,typdecl) env in
+      (newenv,(name::idl)))
+    ctxt (pf_env gl , []) in
+  List.rev res 
+
+
 let build_intro_tac id = function
   | None      -> introduction id
   | Some dest -> tclTHEN (introduction id) (move_hyp true id dest)
@@ -427,12 +447,9 @@ let rec intros_rmove = function
  		    move_to_rhyp destopt;
 		    intros_rmove rest ]
 
-(****************************************************)
-(*            Resolution tactics                    *)
-(****************************************************)
-
-(*  Refinement tactic: unification with the head of the head normal form
- *  of the type of a term. *)
+(**************************)
+(*  Refinement tactics    *)
+(**************************)
 
 let apply_type hdcty argl gl =
   refine (applist (mkCast (Evarutil.mk_new_meta(),DEFAULTcast, hdcty),argl)) gl
@@ -448,6 +465,48 @@ let bring_hyps hyps =
       let f = mkCast (Evarutil.mk_new_meta(),DEFAULTcast, newcl) in
       refine_no_check (mkApp (f, instance_from_named_context hyps)) gl)
 
+(**************************)
+(*     Cut tactics        *)
+(**************************)
+
+let cut c gl =
+  match kind_of_term (hnf_type_of gl c) with
+    | Sort _ ->
+        let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
+        let t = mkProd (Anonymous, c, pf_concl gl) in
+          tclTHENFIRST
+            (internal_cut_rev id c)
+            (tclTHEN (apply_type t [mkVar id]) (thin [id]))
+            gl
+    | _  -> error "Not a proposition or a type"
+
+let cut_intro t = tclTHENFIRST (cut t) intro
+
+(* let cut_replacing id t tac = 
+  tclTHENS (cut t)
+    [tclORELSE
+	(intro_replacing id) 
+	(tclORELSE (intro_erasing id) (intro_using id));
+     tac (refine_no_check (mkVar id)) ] *)
+
+(* cut_replacing échoue si l'hypothèse à remplacer apparaît dans le
+   but, ou dans une autre hypothèse *)
+let cut_replacing id t tac = 
+  tclTHENS (cut t) [
+      tclORELSE (intro_replacing id) (intro_erasing id); 
+      tac (refine_no_check (mkVar id)) ]
+
+let cut_in_parallel l = 
+  let rec prec = function
+    | [] -> tclIDTAC 
+    | h::t -> tclTHENFIRST (cut h) (prec t)
+  in 
+    prec (List.rev l)
+
+(****************************************************)
+(*            Resolution tactics                    *)
+(****************************************************)
+
 (* Resolution with missing arguments *)
 
 let apply_with_bindings (c,lbind) gl = 
@@ -459,7 +518,7 @@ let apply_with_bindings (c,lbind) gl =
     try
       let n = nb_prod thm_ty - nb_prod (pf_concl gl) in
       if n<0 then error "Apply: theorem has not enough premisses.";
-      let clause = make_clenv_binding_apply gl n (c,thm_ty) lbind in
+      let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
       Clenvtac.res_pf clause gl
     with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) as exn ->
       let red_thm =
@@ -470,7 +529,7 @@ let apply_with_bindings (c,lbind) gl =
   with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) ->
     (* Last chance: if the head is a variable, apply may try
        second order unification *)
-    let clause = make_clenv_binding_apply gl (-1) (c,thm_ty0) lbind in 
+    let clause = make_clenv_binding_apply gl None (c,thm_ty0) lbind in 
     Clenvtac.res_pf clause gl
 
 let apply c = apply_with_bindings (c,NoBindings)
@@ -485,6 +544,44 @@ let apply_without_reduce c gl =
   let clause = mk_clenv_type_of gl c in 
   res_pf clause gl
 
+(* [apply_in hyp c] replaces
+
+   hyp : forall y1, ti -> t             hyp : rho(u)
+   ========================    with     ============  and the =======
+   goal                                 goal                  rho(ti)
+
+   assuming that [c] has type [forall x1..xn -> t' -> u] for some [t]
+   unifiable with [t'] with unifier [rho]
+*)
+
+let find_matching_clause unifier clause =
+  let rec find clause =
+    try unifier clause
+    with exn when catchable_exception exn ->
+    try find (clenv_push_prod clause)
+    with NotExtensibleClause -> failwith "Cannot apply"
+  in find clause
+
+let apply_in_once gls innerclause (d,lbind) =
+  let thm = nf_betaiota (pf_type_of gls d) in
+  let clause = make_clenv_binding gls (d,thm) lbind in
+  let ordered_metas = List.rev (clenv_independent clause) in
+  if ordered_metas = [] then error "Statement without assumptions";
+  let f mv = find_matching_clause (clenv_fchain mv clause) innerclause in
+  try list_try_find f ordered_metas
+  with Failure _ -> error "Unable to unify"
+
+let apply_in id lemmas gls =
+  let t' = pf_get_hyp_typ gls id in
+  let innermostclause = mk_clenv_from_n gls (Some 0) (mkVar id,t') in
+  let clause = List.fold_left (apply_in_once gls) innermostclause lemmas in
+  let new_hyp_prf  = clenv_value clause in
+  let new_hyp_typ  = clenv_type clause in
+  tclTHEN
+    (tclEVARS (evars_of clause.env))
+    (cut_replacing id new_hyp_typ
+      (fun x gls -> refine_no_check new_hyp_prf gls)) gls
+
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
    |- B -> C and |- A
 
@@ -502,45 +599,14 @@ let apply_without_reduce c gl =
   end.
 *)
 
-(**************************)
-(*     Cut tactics        *)
-(**************************)
-
 let cut_and_apply c gl =
   let goal_constr = pf_concl gl in 
-  match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with
-    | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
-	tclTHENLAST
-	  (apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())])
-	  (apply_term c [mkMeta (new_meta())]) gl
-    | _ -> error "Imp_elim needs a non-dependent product"
-
-let cut c gl =
-  match kind_of_term (hnf_type_of gl c) with
-    | Sort _ ->
-        let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
-        let t = mkProd (Anonymous, c, pf_concl gl) in
-        tclTHENFIRST
-          (internal_cut_rev id c)
-          (tclTHEN (apply_type t [mkVar id]) (thin [id]))
-          gl
-    | _  -> error "Not a proposition or a type"
-
-let cut_intro t = tclTHENFIRST (cut t) intro
-
-let cut_replacing id t tac = 
-  tclTHENS (cut t)
-    [tclORELSE
-      (intro_replacing id) 
-      (tclORELSE (intro_erasing id) (intro_using id));
-     tac (refine_no_check (mkVar id)) ]
-
-let cut_in_parallel l = 
-  let rec prec = function
-    | [] -> tclIDTAC 
-    | h::t -> tclTHENFIRST (cut h) (prec t)
-  in 
-  prec (List.rev l)
+    match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with
+      | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
+	  tclTHENLAST
+	    (apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())])
+	    (apply_term c [mkMeta (new_meta())]) gl
+      | _ -> error "Imp_elim needs a non-dependent product"
 
 (********************************************************************)
 (*               Exact tactics                                      *)
@@ -717,7 +783,7 @@ let general_elim_clause elimtac (c,lbindc) (elimc,lbindelimc) gl =
   let indclause  = make_clenv_binding gl (c,t) lbindc  in
   let elimt      = pf_type_of gl elimc in
   let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in 
-  elimtac elimclause indclause gl
+    elimtac elimclause indclause gl
 
 let general_elim c e ?(allow_K=true) =
   general_elim_clause (elimination_clause_scheme allow_K) c e
@@ -747,6 +813,14 @@ let elim (c,lbindc as cx) elim =
 let simplest_elim c = default_elim (c,NoBindings)
 
 (* Elimination in hypothesis *)
+(* Typically, elimclause := (eq_ind ?x ?P ?H ?y ?Heq : ?P ?y)
+              indclause : forall ..., hyps -> a=b    (to take place of ?Heq)
+              id : phi(a)                            (to take place of ?H)
+      and the result is to overwrite id with the proof of phi(b)
+
+   but this generalizes to any elimination scheme with one constructor
+   (e.g. it could replace id:A->B->C by id:C, knowing A/\B)
+*)
 
 let elimination_in_clause_scheme id elimclause indclause gl =
   let (hypmv,indmv) = 
@@ -757,8 +831,7 @@ let elimination_in_clause_scheme id elimclause indclause gl =
   let elimclause'  = clenv_fchain indmv elimclause indclause in 
   let hyp = mkVar id in
   let hyp_typ = pf_type_of gl hyp in
-  let hypclause =
-    mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
+  let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
   let elimclause'' = clenv_fchain hypmv elimclause' hypclause in  
   let new_hyp_prf  = clenv_value elimclause'' in
   let new_hyp_typ  = clenv_type elimclause'' in
@@ -1145,13 +1218,18 @@ let consume_pattern avoid id gl = function
       (IntroIdentifier (fresh_id avoid id gl), names)
   | pat::names -> (pat,names)
 
+let re_intro_dependent_hypotheses tophyp (lstatus,rstatus) =
+  let newlstatus = (* if some IH has taken place at the top of hyps *)
+    List.map (function (hyp,None) -> (hyp,tophyp) | x -> x) lstatus in
+  tclTHEN
+    (intros_rmove rstatus)
+    (intros_move newlstatus)
+
 type elim_arg_kind = RecArg | IndArg | OtherArg
 
 let induct_discharge statuslists destopt avoid' (avoid,ra) names gl =
   let avoid = avoid @ avoid' in
-  let (lstatus,rstatus) = statuslists in
-  let tophyp = ref None in
-  let rec peel_tac ra names gl = match ra with
+  let rec peel_tac ra names tophyp gl = match ra with
     | (RecArg,recvarname) ::
         (IndArg,hyprecname) :: ra' ->
         let recpat,names = match names with
@@ -1160,36 +1238,35 @@ let induct_discharge statuslists destopt avoid' (avoid,ra) names gl =
 	      (pat, [IntroIdentifier id])
           | _ -> consume_pattern avoid recvarname gl names in
         let hyprec,names = consume_pattern avoid hyprecname gl names in
-	(* This is buggy for intro-or-patterns with different first hypnames *)
-	if !tophyp=None then tophyp := first_name_buggy hyprec;
+        (* IH stays at top: we need to update tophyp *)
+        (* This is buggy for intro-or-patterns with different first hypnames *)
+        (* Would need to pass peel_tac as a continuation of intros_patterns *)
+        (* (or to have hypotheses classified by blocks...) *)
+        let tophyp = if tophyp=None then first_name_buggy hyprec else tophyp in
         tclTHENLIST
 	  [ intros_patterns avoid [] destopt [recpat];
 	    intros_patterns avoid [] None [hyprec];
-	    peel_tac ra' names ] gl
+	    peel_tac ra' names tophyp] gl
     | (IndArg,hyprecname) :: ra' ->
 	(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
         let pat,names = consume_pattern avoid hyprecname gl names in
-	tclTHEN (intros_patterns avoid [] destopt [pat]) (peel_tac ra' names) gl
+	tclTHEN (intros_patterns avoid [] destopt [pat])
+          (peel_tac ra' names tophyp) gl
     | (RecArg,recvarname) :: ra' ->
         let pat,names = consume_pattern avoid recvarname gl names in
-	tclTHEN (intros_patterns avoid [] destopt [pat]) (peel_tac ra' names) gl
+	tclTHEN (intros_patterns avoid [] destopt [pat]) 
+          (peel_tac ra' names tophyp) gl
     | (OtherArg,_) :: ra' ->
         let pat,names = match names with
           | [] -> IntroAnonymous, []
           | pat::names -> pat,names in
-	tclTHEN (intros_patterns avoid [] destopt [pat]) (peel_tac ra' names) gl
+	tclTHEN (intros_patterns avoid [] destopt [pat])
+          (peel_tac ra' names tophyp) gl
     | [] ->
         check_unused_names names;
-        tclIDTAC gl
+        re_intro_dependent_hypotheses tophyp statuslists gl
   in
-  let intros_move lstatus =
-    let newlstatus = (* if some IH has taken place at the top of hyps *)
-      List.map (function (hyp,None) -> (hyp,!tophyp) | x -> x) lstatus in
-    intros_move newlstatus
-  in 
-  tclTHENLIST [ peel_tac ra names;
-		intros_rmove rstatus;
-		intros_move lstatus ] gl
+  peel_tac ra names None gl
 
 (* - le recalcul de indtyp à chaque itération de atomize_one est pour ne pas
      s'embêter à regarder si un letin_tac ne fait pas des
@@ -1648,8 +1725,13 @@ let compute_elim_sig ?elimc elimt =
 	| hiname,Some _,hi -> error "cannot recognize an induction schema"
 	| hiname,None,hi -> 
 	    let hi_ind, hi_args = decompose_app hi in
-	    let hi_is_ind = (* hi est d'un type inductif *)
-	      match kind_of_term hi_ind with | Ind (mind,_)  -> true | _ -> false in
+	    let hi_is_ind = (* hi est d'un type globalisable *)
+	      match kind_of_term hi_ind with
+		| Ind (mind,_)  -> true 
+		| Var _ -> true 
+		| Const _ -> true 
+		| Construct _ -> true 
+		| _ -> false in
 	    let hi_args_enough = (* hi a le bon nbre d'arguments *)
 	      List.length hi_args = List.length params + !res.nargs -1 in
 	    (* FIXME: Ces deux tests ne sont pas suffisants. *)
@@ -1827,6 +1909,7 @@ let recolle_clenv scheme lid elimclause gl =
     elimclause
 
 
+
 (* Unification of the goal and the principle applied to meta variables:
    (elimc ?i ?j ?k...?l). This solves partly meta variables (and may
     produce new ones). Then refine with the resulting term with holes.
@@ -1858,7 +1941,7 @@ let induction_from_context_l isrec elim_info lid names gl =
     + (if scheme.indarg <> None then 1 else 0) in
   (* Number of given induction args must be exact. *)
   if List.length lid <> nargs_indarg_farg + scheme.nparams then 
-    error "not the right number of arguments given to induction scheme";  
+      error "not the right number of arguments given to induction scheme";  
   let env = pf_env gl in
   (* hyp0 is used for re-introducing hyps at the right place afterward.
      We chose the first element of the list of variables on which to
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index aaacee8f..48b9f432 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 8878 2006-05-30 16:44:25Z herbelin $ i*)
+(*i $Id: tactics.mli 9266 2006-10-24 09:03:15Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -58,6 +58,7 @@ val cofix           : identifier option -> tactic
 (*s Introduction tactics. *)
 
 val fresh_id : identifier list -> identifier -> goal sigma -> identifier
+val find_intro_names : rel_context -> goal sigma -> identifier list
 
 val intro                : tactic
 val introf               : tactic
@@ -168,6 +169,8 @@ val apply_with_bindings   : constr with_bindings -> tactic
 
 val cut_and_apply         : constr -> tactic
 
+val apply_in              : identifier -> constr with_bindings list -> tactic
+
 (*s Elimination tactics. *)