Integrate a few improvements on typeclasses and Program from the equations branch

and remove equations stuff which moves to a separate plugin.

Classes:
- Ability to define classes post-hoc from constants or inductive types.
- Correctly rebuild the hint database associated to local hypotheses when 
  they are changed by a [Hint Extern] in typeclass resolution.

Tactics and proofs:
- Change [revert] so that it keeps let-ins (but not [generalize]).
- Various improvements to the [generalize_eqs] tactic to make it more robust
  and produce the smallest proof terms possible.
  Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with 
  [generalize_eqs].
- A few new general purpose tactics in Program.Tactics like [revert_until]
- Make transitive closure well-foundedness proofs transparent.
- More uniform testing for metas/evars in pretyping/unification.ml
  (might introduce a few changes in the contribs).

Program:
- Better sorting of dependencies in obligations.
- Ability to start a Program definition from just a type and no obligations, 
  automatically adding an obligation for this type.
- In compilation of Program's well-founded definitions, make the functional a
  separate definition for easier reasoning.
- Add a hint database for every Program populated by [Hint Unfold]s for 
  every defined obligation constant.


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

10 files changed, 450 insertions, 201 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index dd11e1ef0e..5de89baa64 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -123,6 +123,7 @@ module Hint_db = struct
 
   type t = {
     hintdb_state : Names.transparent_state;
+    hintdb_unfolds : Idset.t * Cset.t;
     use_dn : bool;
     hintdb_map : search_entry Constr_map.t;
     (* A list of unindexed entries starting with an unfoldable constant
@@ -131,6 +132,7 @@ module Hint_db = struct
   }
 
   let empty st use_dn = { hintdb_state = st;
+			  hintdb_unfolds = (Idset.empty, Cset.empty);
 			  use_dn = use_dn;
 			  hintdb_map = Constr_map.empty;
 			  hintdb_nopat = [] }
@@ -179,14 +181,17 @@ module Hint_db = struct
       List.fold_left (fun db (gr,v) -> addkv gr v db) db' db.hintdb_nopat
 
   let add_one (k,v) db =
-    let st',rebuild =
+    let st',db,rebuild =
       match v.code with
       | Unfold_nth egr ->
-	  let (ids,csts) = db.hintdb_state in
-	    (match egr with
-	    | EvalVarRef id -> (Idpred.add id ids, csts)
-	    | EvalConstRef cst -> (ids, Cpred.add cst csts)), true
-      | _ -> db.hintdb_state, false
+	  let addunf (ids,csts) (ids',csts') =
+	    match egr with
+	    | EvalVarRef id -> (Idpred.add id ids, csts), (Idset.add id ids', csts')
+	    | EvalConstRef cst -> (ids, Cpred.add cst csts), (ids', Cset.add cst csts')
+	  in 
+	  let state, unfs = addunf db.hintdb_state db.hintdb_unfolds in
+	    state, { db with hintdb_unfolds = unfs }, true
+      | _ -> db.hintdb_state, db, false
     in
     let db = if db.use_dn && rebuild then rebuild_db st' db else db
     in addkv k v db
@@ -203,6 +208,8 @@ module Hint_db = struct
     if db.use_dn then rebuild_db st db
     else { db with hintdb_state = st }
 
+  let unfolds db = db.hintdb_unfolds
+
   let use_dn db = db.use_dn
 
 end
@@ -356,17 +363,18 @@ open Vernacexpr
 
 (* If the database does not exist, it is created *)
 (* TODO: should a warning be printed in this case ?? *)
-let add_hint dbname hintlist =
-  try
-    let db = searchtable_map dbname in
-    let db' = Hint_db.add_list hintlist db in
+
+let get_db dbname =
+  try searchtable_map dbname
+  with Not_found -> Hint_db.empty empty_transparent_state false
+
+let add_hint dbname hintlist = 
+  let db = get_db dbname in
+  let db' = Hint_db.add_list hintlist db in
     searchtable_add (dbname,db')
-  with Not_found ->
-    let db = Hint_db.add_list hintlist (Hint_db.empty empty_transparent_state false) in
-    searchtable_add (dbname,db)
 
 let add_transparency dbname grs b =
-  let db = searchtable_map dbname in
+  let db = get_db dbname in
   let st = Hint_db.transparent_state db in
   let st' =
     List.fold_left (fun (ids, csts) gr ->
@@ -882,7 +890,7 @@ and tac_of_hint db_list local_db concl (flags, {pat=p; code=t}) =
       tclTHEN
         (unify_resolve_gen flags (term,cl))
         (trivial_fail_db (flags <> None) db_list local_db)
-  | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
+  | Unfold_nth c -> tclPROGRESS (unfold_in_concl [all_occurrences,c])
   | Extern tacast -> conclPattern concl p tacast
 
 and trivial_resolve mod_delta db_list local_db cl =
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 83ad60bc30..fe59dc1e12 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -63,6 +63,8 @@ module Hint_db :
     val use_dn : t -> bool
     val transparent_state : t -> transparent_state
     val set_transparent_state : t -> transparent_state -> t
+
+    val unfolds : t -> Idset.t * Cset.t
   end
 
 type hint_db_name = string
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index db0bbd867a..0b69eebbd6 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -247,7 +247,9 @@ type hypinfo = {
 }
 
 let evd_convertible env evd x y =
-  try ignore(Evarconv.the_conv_x env x y evd); true
+  try
+    ignore(Unification.w_unify true env Reduction.CONV x y evd); true 
+  (* try ignore(Evarconv.the_conv_x env x y evd); true *)
   with _ -> false
 
 let decompose_applied_relation metas env sigma c ctype left2right =
@@ -269,8 +271,8 @@ let decompose_applied_relation metas env sigma c ctype left2right =
 	let ty1, ty2 =
 	  Typing.mtype_of env eqclause.evd c1, Typing.mtype_of env eqclause.evd c2
 	in
-	  if not (evd_convertible env eqclause.evd ty1 ty2) then None
-	  else
+(* 	  if not (evd_convertible env eqclause.evd ty1 ty2) then None *)
+(* 	  else *)
 	    Some { hyp_cl=eqclause; hyp_prf=(Clenv.clenv_value eqclause); hyp_ty = ty;
 		   hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others);
 		   hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; }
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 94b2eff387..40eaec65c6 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -89,13 +89,10 @@ let intersects s t =
 
 open Auto
 
-let e_give_exact flags c gl =
-  let t1 = (pf_type_of gl c) and t2 = pf_concl gl in
-    if occur_existential t1 or occur_existential t2 then
-      tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl
-    else exact_check c gl
-(*   let t1 = (pf_type_of gl c) in *)
-(*     tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl *)
+let e_give_exact flags c gl = 
+  let t1 = (pf_type_of gl c) in
+    tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl
+
 let assumption flags id = e_give_exact flags (mkVar id)
 
 open Unification
@@ -129,12 +126,12 @@ END
 let unify_e_resolve flags (c,clenv) gls =
   let clenv' = connect_clenv gls clenv in
   let clenv' = clenv_unique_resolver false ~flags clenv' gls in
-    Clenvtac.clenv_refine true ~with_classes:false clenv' gls
+    tclPROGRESS (Clenvtac.clenv_refine true ~with_classes:false clenv') gls
 
 let unify_resolve flags (c,clenv) gls =
   let clenv' = connect_clenv gls clenv in
   let clenv' = clenv_unique_resolver false ~flags clenv' gls in
-    Clenvtac.clenv_refine false ~with_classes:false clenv' gls
+    tclPROGRESS (Clenvtac.clenv_refine false ~with_classes:false clenv') gls
 
 (** Hack to properly solve dependent evars that are typeclasses *)
 
@@ -151,9 +148,9 @@ let rec e_trivial_fail_db db_list local_db goal =
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
           (e_trivial_fail_db db_list
 	      (Hint_db.add_list hintl local_db) g'))) ::
-    (List.map pi1 (e_trivial_resolve db_list local_db (pf_concl goal)) )
-  in
-  tclFIRST (List.map tclCOMPLETE tacl) goal
+    (List.map (fun (x,_,_,_) -> x) (e_trivial_resolve db_list local_db (pf_concl goal)))
+  in 
+  tclFIRST (List.map tclCOMPLETE tacl) goal 
 
 and e_my_find_search db_list local_db hdc concl =
   let hdc = head_of_constr_reference hdc in
@@ -178,12 +175,13 @@ and e_my_find_search db_list local_db hdc concl =
 	  | Res_pf_THEN_trivial_fail (term,cl) ->
               tclTHEN (unify_e_resolve flags (term,cl))
 		(e_trivial_fail_db db_list local_db)
-	  | Unfold_nth c -> unfold_in_concl [all_occurrences,c]
+	  | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [all_occurrences,c])
 	  | Extern tacast -> conclPattern concl p tacast
       in
-	(tac,b,pr_autotactic t)
-  in
-    List.map tac_of_hint hintl
+	match t with
+	| Extern _ -> (tac,b,true,pr_autotactic t)
+	| _ -> (tac,b,false,pr_autotactic t)
+  in List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db gl =
   try
@@ -228,7 +226,7 @@ type validation = evar_map -> proof_tree list -> proof_tree
 
 let pr_depth l = prlist_with_sep (fun () -> str ".") pr_int (List.rev l)
 
-type autoinfo = { hints : Auto.hint_db; auto_depth: int list; auto_last_tac: std_ppcmds }
+type autoinfo = { hints : Auto.hint_db; only_classes: bool; auto_depth: int list; auto_last_tac: std_ppcmds }
 type autogoal = goal * autoinfo
 type 'ans fk = unit -> 'ans
 type ('a,'ans) sk = 'a -> 'ans fk -> 'ans
@@ -238,6 +236,26 @@ type auto_result = autogoal list sigma * validation
 
 type atac = auto_result tac
 
+let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
+  let cty = Evarutil.nf_evar sigma cty in
+  let keep = not only_classes || 
+    let ctx, ar = decompose_prod cty in
+      match kind_of_term (fst (decompose_app ar)) with
+      | Const c -> is_class (ConstRef c)
+      | Ind i -> is_class (IndRef i)
+      | _ -> false
+  in
+    if keep then let c = mkVar id in
+      map_succeed 
+	(fun f -> try f (c,cty) with UserError _ -> failwith "") 
+	[make_exact_entry pri; make_apply_entry env sigma flags pri]
+    else []
+
+let make_autogoal_hints only_classes ?(st=full_transparent_state) g =
+  let sign = pf_hyps g in
+  let hintlist = list_map_append (pf_apply make_resolve_hyp g st (true,false,false) only_classes None) sign in
+    Hint_db.add_list hintlist (Hint_db.empty st true)
+  
 let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac =
   { skft = fun sk fk {it = gl,hints; sigma=s} ->
     let res = try Some (tac {it=gl; sigma=s}) with e when catchable e -> None in
@@ -251,7 +269,8 @@ let intro_tac : atac =
       let gls' =
 	List.map (fun g' ->
 	  let env = evar_env g' in
-	  let hint = make_resolve_hyp env s (List.hd (evar_context g')) in
+	  let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints) 
+	    (true,false,false) info.only_classes None (List.hd (evar_context g')) in
 	  let ldb = Hint_db.add_list hint info.hints in
 	    (g', { info with hints = ldb; auto_last_tac = str"intro" })) gls
       in {it = gls'; sigma = s})
@@ -261,7 +280,7 @@ let id_tac : atac =
     sk ({it = [gl]; sigma = s}, fun _ pfs -> List.hd pfs) fk }
 
 (* Ordering of states is lexicographic on the number of remaining goals. *)
-let compare (pri, _, (res, _)) (pri', _, (res', _)) =
+let compare (pri, _, _, (res, _)) (pri', _, _, (res', _)) =
   let nbgoals s =
     List.length (sig_it s) + nb_empty_evars (sig_sig s)
   in
@@ -277,17 +296,17 @@ let solve_tac (x : 'a tac) : 'a tac =
 
 let hints_tac hints =
   { skft = fun sk fk {it = gl,info; sigma = s} ->
-(*     if !typeclasses_debug then msgnl (str"depth=" ++ int info.auto_depth ++ str": " ++ info.auto_last_tac *)
-(* 					 ++ spc () ++ str "->" ++ spc () ++ pr_ev s gl); *)
-    let possible_resolve ((lgls,v) as res, pri, pp) =
-      (pri, pp, res)
+    let possible_resolve ((lgls,v) as res, pri, b, pp) =
+      (pri, pp, b, res)
     in
+    let ({it = normalized; sigma = s}, valid) = tclNORMEVAR {it = gl; sigma = s} in
+    let gl = List.hd normalized in
     let tacs =
       let concl = Evarutil.nf_evar s gl.evar_concl in
       let poss = e_possible_resolve hints info.hints concl in
       let l =
-	Util.list_map_append (fun (tac, pri, pptac) ->
-	  try [tac {it = gl; sigma = s}, pri, pptac] with e when catchable e -> [])
+	Util.list_map_append (fun (tac, pri, b, pptac) ->
+	  try [(tclTHEN tclNORMEVAR tac) {it = gl; sigma = s}, pri, b, pptac] with e when catchable e -> [])
 	  poss
       in
 	if l = [] && !typeclasses_debug then
@@ -298,16 +317,24 @@ let hints_tac hints =
     in
     let tacs = List.sort compare tacs in
     let rec aux i = function
-      | (_, pp, ({it = gls; sigma = s}, v)) :: tl ->
+      | (_, pp, b, ({it = gls; sigma = s}, v)) :: tl ->
 	  if !typeclasses_debug then msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ pp
 					       ++ str" on" ++ spc () ++ pr_ev s gl);
 	  let fk =
 	    (fun () -> (* if !typeclasses_debug then msgnl (str"backtracked after " ++ pp); *)
 	    aux (succ i) tl)
 	  in
-	  let glsv = {it = list_map_i (fun j g -> g,
-	    { info with auto_depth = j :: i :: info.auto_depth;
-	      auto_last_tac = pp }) 1 gls; sigma = s}, fun _ -> v in
+	  let gls' = list_map_i (fun j g -> 
+	    let info = 
+	      { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp;
+		hints = 
+		  if b && g.evar_hyps <> gl.evar_hyps 
+		  then make_autogoal_hints info.only_classes
+		    ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s}
+		  else info.hints }
+	    in g, info) 1 gls in
+	  let glsvalid _ pfs = valid [v pfs] in
+	  let glsv = {it = gls'; sigma = s}, glsvalid in
 	    sk glsv fk
       | [] -> fk ()
     in aux 1 tacs }
@@ -351,42 +378,13 @@ let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res
 let rec fix (t : 'a tac) : 'a tac =
   then_tac t { skft = fun sk fk -> (fix t).skft sk fk }
 
-
-(* A special one for getting everything into a dnet. *)
-
-let is_transparent_gr (ids, csts) = function
-  | VarRef id -> Idpred.mem id ids
-  | ConstRef cst -> Cpred.mem cst csts
-  | IndRef _ | ConstructRef _ -> false
-
-let make_resolve_hyp env sigma st flags pri (id, _, cty) =
-  let cty = Evarutil.nf_evar sigma cty in
-  let ctx, ar = decompose_prod cty in
-  let keep =
-    match kind_of_term (fst (decompose_app ar)) with
-    | Const c -> is_class (ConstRef c)
-    | Ind i -> is_class (IndRef i)
-    | _ -> false
-  in
-    if keep then let c = mkVar id in
-      map_succeed
-	(fun f -> f (c,cty))
-	[make_exact_entry pri; make_apply_entry env sigma flags pri]
-    else []
-
-let make_autogoal ?(st=full_transparent_state) g =
-  let sign = pf_hyps g in
-  let hintlist = list_map_append (pf_apply make_resolve_hyp g st (true,false,false) None) sign in
-  let st = List.fold_left (fun (ids, csts) (n, b, t) ->
-    (if b <> None then Idpred.add else Idpred.remove) n ids, csts)
-    st sign
-  in
-  let hints = Hint_db.add_list hintlist (Hint_db.empty st true) in
-    (g.it, { hints = hints ; auto_depth = []; auto_last_tac = mt() })
-
-let make_autogoals ?(st=full_transparent_state) gs evm' =
-  { it = list_map_i (fun i g ->
-    let (gl, auto) = make_autogoal ~st {it = snd g; sigma = evm'} in
+let make_autogoal ?(only_classes=true) ?(st=full_transparent_state) g =
+  let hints = make_autogoal_hints only_classes ~st g in
+    (g.it, { hints = hints ; only_classes = only_classes; auto_depth = []; auto_last_tac = mt() })
+      
+let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) gs evm' =
+  { it = list_map_i (fun i g -> 
+    let (gl, auto) = make_autogoal ~only_classes ~st {it = snd g; sigma = evm'} in
       (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm' }
 
 let get_result r = 
@@ -395,20 +393,20 @@ let get_result r =
   | Some ((gls, v), fk) ->
       try ignore(v (sig_sig gls) []); assert(false)
       with Found evm' -> Some (evm', fk)
-	
-let run_on_evars ?(st=full_transparent_state) p evm tac =
+
+let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm tac =
   match evars_to_goals p evm with
   | None -> None (* This happens only because there's no evar having p *)
   | Some (goals, evm') ->
-      let res = run_list_tac tac p goals (make_autogoals ~st goals evm') in
+      let res = run_list_tac tac p goals (make_autogoals ~only_classes ~st goals evm') in
 	match get_result res with
 	| None -> raise Not_found
 	| Some (evm', fk) -> Some (Evd.evars_reset_evd evm' evm, fk)
-
+	    
 let eauto_tac hints = fix (or_tac intro_tac (hints_tac hints))
-
-let eauto hints g =
-  let gl = { it = make_autogoal ~st:(Hint_db.transparent_state (List.hd hints)) g; sigma = project g } in
+  
+let eauto ?(only_classes=true) ?st hints g =
+  let gl = { it = make_autogoal ~only_classes ?st g; sigma = project g } in
     match run_tac (eauto_tac hints) gl with
     | None -> raise Not_found
     | Some ({it = goals; sigma = s}, valid) ->
@@ -477,6 +475,27 @@ let select_evars evs evm =
     if Intset.mem ev evs then Evd.add acc ev evi else acc)
     evm Evd.empty
 
+let is_inference_forced p ev evd =
+  try
+    let evi = Evd.find evd ev in
+      if evi.evar_body = Evar_empty then
+	if Typeclasses.is_resolvable evi
+	  && snd (p ev evi)
+	then
+	  let (loc, k) = evar_source ev evd in
+	    match k with
+	    | ImplicitArg (_, _, b) -> b
+	    | QuestionMark _ -> false
+	    | _ -> true
+	else true
+      else false
+  with Not_found -> true
+
+let is_optional p comp evd =
+  Intset.fold (fun ev acc ->
+    acc && not (is_inference_forced p ev evd))
+    comp true
+
 let resolve_all_evars debug m env p oevd do_split fail =
   let split = if do_split then split_evars oevd else [Intset.empty] in
   let p = if do_split then
@@ -506,10 +525,10 @@ let resolve_all_evars debug m env p oevd do_split fail =
     | comp :: comps ->
 	let res = try aux (p comp) evd with Not_found -> None in
 	  match res with
-	  | None ->
-	      if fail then
+	  | None -> 
+	      if fail && (not do_split || not (is_optional (p comp evd) comp evd)) then
+		(* Unable to satisfy the constraints. *)		
 		let evd = Evarutil.nf_evars evd in
-		(* Unable to satisfy the constraints. *)
 		let evm = if do_split then select_evars comp evd else evd in
 		let _, ev = Evd.fold
 		  (fun ev evi (b,acc) ->
@@ -540,19 +559,20 @@ let _ =
   Typeclasses.solve_instanciations_problem :=
     solve_inst false true default_eauto_depth
 
+let set_transparency cl b =
+  List.iter (fun r -> 
+    let gr = Smartlocate.global_with_alias r in
+    let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in
+      Classes.set_typeclass_transparency ev b) cl
 
 VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings
 | [ "Typeclasses" "Transparent" reference_list(cl) ] -> [
-    add_hints false [typeclasses_db]
-      (interp_hints (Vernacexpr.HintsTransparency (cl, true)))
-  ]
+    set_transparency cl true ]
 END
 
 VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings
 | [ "Typeclasses" "Opaque" reference_list(cl) ] -> [
-    add_hints false [typeclasses_db]
-      (interp_hints (Vernacexpr.HintsTransparency (cl, false)))
-  ]
+    set_transparency cl false ]
 END
 
 open Genarg
@@ -596,10 +616,16 @@ VERNAC COMMAND EXTEND Typeclasses_Settings
    ]
 END
 
+let typeclasses_eauto ?(st=full_transparent_state) dbs gl =
+  try 
+    let dbs = list_map_filter (fun db -> try Some (Auto.searchtable_map db) with _ -> None) dbs in
+    let st = match dbs with [x] -> Hint_db.transparent_state x | _ -> st in
+	eauto ~only_classes:false ~st dbs gl
+  with Not_found -> tclFAIL 0 (str" typeclasses eauto failed") gl
+
 TACTIC EXTEND typeclasses_eauto
-| [ "typeclasses" "eauto" ] -> [ fun gl ->
-    try eauto [Auto.searchtable_map typeclasses_db] gl
-    with Not_found -> tclFAIL 0 (str" typeclasses eauto failed") gl ]
+| [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ typeclasses_eauto l ]
+| [ "typeclasses" "eauto" ] -> [ typeclasses_eauto [typeclasses_db] ]
 END
 
 let _ = Classes.refine_ref := Refine.refine
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 25efd5a050..17361f2e65 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -394,6 +394,18 @@ TACTIC EXTEND dfs_eauto
     [ gen_eauto false (true, make_depth p) lems db ]
 END
 
+let cons a l = a :: l
+
+let autounfold db cl =
+  let unfolds = List.concat (List.map (fun dbname -> 
+    let db = try searchtable_map dbname 
+      with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+    in
+    let (ids, csts) = Hint_db.unfolds db in
+      Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts
+	(Idset.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db)
+  in unfold_option unfolds cl
+
 let autosimpl db cl =
   let unfold_of_elts constr (b, elts) =
     if not b then
@@ -407,9 +419,86 @@ let autosimpl db cl =
       unfold_of_elts (fun x -> EvalVarRef x) (Idpred.elements ids)) db)
   in unfold_option unfolds cl
 
-TACTIC EXTEND autosimpl
-| [ "autosimpl" hintbases(db) ] ->
-    [ autosimpl (match db with None -> ["core"] | Some x -> "core"::x) None ]
+TACTIC EXTEND autounfold
+| [ "autounfold" hintbases(db) "in" hyp(id) ] ->
+    [ autounfold (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, InHyp)) ]
+| [ "autounfold" hintbases(db) ] ->
+    [ autounfold (match db with None -> ["core"] | Some x -> "core"::x) None ]
+      END
+
+let unfold_head env (ids, csts) c = 
+  let rec aux c = 
+    match kind_of_term c with
+    | Var id when Idset.mem id ids ->
+	(match Environ.named_body id env with
+	| Some b -> true, b
+	| None -> false, c)
+    | Const cst when Cset.mem cst csts ->
+	true, Environ.constant_value env cst
+    | App (f, args) ->
+	(match aux f with
+	| true, f' -> true, Reductionops.whd_betaiota Evd.empty (mkApp (f', args))
+	| false, _ -> 
+	    let done_, args' = 
+	      array_fold_left_i (fun i (done_, acc) arg -> 
+		if done_ then done_, arg :: acc 
+		else match aux arg with
+		| true, arg' -> true, arg' :: acc
+		| false, arg' -> false, arg :: acc)
+		(false, []) args
+	    in 
+	      if done_ then true, mkApp (f, Array.of_list (List.rev args'))
+	      else false, c)
+    | _ -> 
+	let done_ = ref false in
+	let c' = map_constr (fun c -> 
+	  if !done_ then c else 
+	    let x, c' = aux c in
+	      done_ := x; c') c
+	in !done_, c'
+  in aux c
+
+let autounfold_one db cl gl =
+  let st =
+    List.fold_left (fun (i,c) dbname -> 
+      let db = try searchtable_map dbname 
+	with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+      in
+      let (ids, csts) = Hint_db.unfolds db in
+	(Idset.union ids i, Cset.union csts c)) (Idset.empty, Cset.empty) db
+  in
+  let did, c' = unfold_head (pf_env gl) st (match cl with Some (id, _) -> pf_get_hyp_typ gl id | None -> pf_concl gl) in
+    if did then
+      match cl with
+      | Some hyp -> change_in_hyp None c' hyp gl
+      | None -> convert_concl_no_check c' DEFAULTcast gl
+    else tclFAIL 0 (str "Nothing to unfold") gl
+
+(* 	  Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts *)
+(* 	    (Idset.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) *)
+(*       in unfold_option unfolds cl *)
+
+(*       let db = try searchtable_map dbname  *)
+(* 	with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname) *)
+(*       in *)
+(*       let (ids, csts) = Hint_db.unfolds db in *)
+(* 	Cset.fold (fun cst -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cst)) csts *)
+(* 	  (Idset.fold (fun id -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cl) ids acc))) *)
+(*       (tclFAIL 0 (mt())) db *)
+      
+TACTIC EXTEND autounfold_one
+| [ "autounfold_one" hintbases(db) "in" hyp(id) ] ->
+    [ autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, InHyp)) ]
+| [ "autounfold_one" hintbases(db) ] ->
+    [ autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None ]
+      END
+
+TACTIC EXTEND autounfoldify
+| [ "autounfoldify" constr(x) ] -> [
+    let db = match kind_of_term x with
+      | Const c -> string_of_label (con_label c)
+      | _ -> assert false
+    in autounfold ["core";db] None ]
 END
 
 TACTIC EXTEND unify
@@ -417,3 +506,8 @@ TACTIC EXTEND unify
 | ["unify" constr(x) constr(y) "with" preident(base)  ] -> [
     unify ~state:(Hint_db.transparent_state (searchtable_map base)) x y ]
 END
+
+
+TACTIC EXTEND convert_concl_no_check
+| ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ]
+END
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 7359d070e0..b708949e08 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -35,3 +35,5 @@ val eauto_with_bases :
   bool ->
   bool * int ->
   Term.constr list -> Auto.hint_db list -> Proof_type.tactic
+
+val autounfold : hint_db_name list -> Tacticals.goal_location -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 58ab6dfa0c..de54453100 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -478,10 +478,24 @@ END
 (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as
   defined by Conor McBride *)
 TACTIC EXTEND generalize_eqs
-| ["generalize_eqs" hyp(id) ] -> [ abstract_generalize id ~generalize_vars:false ]
+| ["generalize_eqs" hyp(id) ] -> [ abstract_generalize ~generalize_vars:false id ]
+END
+TACTIC EXTEND dep_generalize_eqs
+| ["dependent" "generalize_eqs" hyp(id) ] -> [ abstract_generalize ~generalize_vars:false ~force_dep:true id ]
 END
 TACTIC EXTEND generalize_eqs_vars
-| ["generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize id ~generalize_vars:true ]
+| ["generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize ~generalize_vars:true id ]
+END
+TACTIC EXTEND dep_generalize_eqs_vars
+| ["dependent" "generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize ~force_dep:true ~generalize_vars:true id ]
+END
+
+(** Tactic to automatically simplify hypotheses of the form [Π Δ, x_i = t_i -> T] 
+    where [t_i] is closed w.r.t. Δ. Such hypotheses are automatically generated
+    during dependent induction. *)
+
+TACTIC EXTEND specialize_hyp
+[ "specialize_hypothesis" hyp(id) ] -> [ specialize_hypothesis id ]
 END
 
 TACTIC EXTEND dependent_pattern
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 0884b3462c..07de95d8ec 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -201,8 +201,8 @@ let build_signature evars env m (cstrs : 'a option list) (finalcstr : 'a option)
 	      if obj = None then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
 	      else error "build_signature: no constraint can apply on a dependent argument"
 	  else
-	    let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
 	    let ty = Reductionops.nf_betaiota (fst evars) ty in
+	    let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
 	    let evars, relty = mk_relty evars env ty obj in
 	    let newarg = mkApp (Lazy.force respectful, [| ty ; b' ; relty ; arg |]) in
 	      evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs
@@ -1279,8 +1279,8 @@ let add_morphism_infer glob m n =
       let cst = Declare.declare_internal_constant instance_id
 				(Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
-				add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob cst);
-				declare_projection n instance_id (ConstRef cst)
+	add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst));
+	declare_projection n instance_id (ConstRef cst)
     else
       let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	Flags.silently
@@ -1289,7 +1289,7 @@ let add_morphism_infer glob m n =
 	      (fun _ -> function
 		Libnames.ConstRef cst ->
 		  add_instance (Typeclasses.new_instance (Lazy.force proper_class) None
-				   glob cst);
+				   glob (ConstRef cst));
 		  declare_projection n instance_id (ConstRef cst)
 		| _ -> assert false);
 	    Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) ();
@@ -1306,8 +1306,7 @@ let add_morphism glob binders m s n =
   in
   let tac = Tacinterp.interp <:tactic<add_morphism_tactic>> in
     ignore(new_instance ~global:glob binders instance (CRecord (dummy_loc,None,[]))
-	      ~generalize:false ~tac
-	      ~hook:(fun cst -> declare_projection n instance_id (ConstRef cst)) None)
+	      ~generalize:false ~tac ~hook:(declare_projection n instance_id) None)
 
 VERNAC COMMAND EXTEND AddSetoid1
    [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f99da0247b..a740d7bb2b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -648,8 +648,8 @@ let cut c gl =
 
 let cut_intro t = tclTHENFIRST (cut t) intro
 
-(* cut_replacing échoue si l'hypothèse à remplacer apparaît dans le
-   but, ou dans une autre hypothèse *)
+(* 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 =
   tclTHENLAST (internal_cut_rev_replace id t)
     (tac (refine_no_check (mkVar id)))
@@ -1427,14 +1427,14 @@ let generalized_name c t ids cl = function
                constante dont on aurait pu prendre directement le nom *)
 	    named_hd (Global.env()) t Anonymous
 
-let generalize_goal gl i ((occs,c),na) cl =
+let generalize_goal gl i ((occs,c,b),na) cl =
   let t = pf_type_of gl c in
   let decls,cl = decompose_prod_n_assum i cl in
   let dummy_prod = it_mkProd_or_LetIn mkProp decls in
   let newdecls,_ = decompose_prod_n_assum i (subst_term c dummy_prod) in
   let cl' = subst_term_occ occs c (it_mkProd_or_LetIn cl newdecls) in
   let na = generalized_name c t (pf_ids_of_hyps gl) cl' na in
-  mkProd (na,t,cl')
+    mkProd_or_LetIn (na,b,t) cl'
 
 let generalize_dep c gl =
   let env = pf_env gl in
@@ -1457,28 +1457,40 @@ let generalize_dep c gl =
       | _ -> tothin
   in
   let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
-  let cl'' = generalize_goal gl 0 ((all_occurrences,c),Anonymous) cl' in
+  let cl'' = generalize_goal gl 0 ((all_occurrences,c,None),Anonymous) cl' in
   let args = Array.to_list (instance_from_named_context to_quantify_rev) in
   tclTHEN
     (apply_type cl'' (c::args))
     (thin (List.rev tothin'))
     gl
 
-let generalize_gen lconstr gl =
+let generalize_gen_let lconstr gl =
   let newcl =
     list_fold_right_i (generalize_goal gl) 0 lconstr (pf_concl gl) in
-  apply_type newcl (List.map (fun ((_,c),_) -> c) lconstr) gl
+  apply_type newcl (list_map_filter (fun ((_,c,b),_) -> 
+    if b = None then Some c else None) lconstr) gl
 
+let generalize_gen lconstr =
+  generalize_gen_let (List.map (fun ((occs,c),na) ->
+    (occs,c,None),na) lconstr)
+    
 let generalize l =
-  generalize_gen (List.map (fun c -> ((all_occurrences,c),Anonymous)) l)
+  generalize_gen_let (List.map (fun c -> ((all_occurrences,c,None),Anonymous)) l)
 
-let revert hyps gl =
-  tclTHEN (generalize (List.map mkVar hyps)) (clear hyps) gl
+let pf_get_hyp_val gl id =
+  let (_, b, _) = pf_get_hyp gl id in
+    b
+
+let revert hyps gl = 
+  let lconstr = List.map (fun id -> 
+    ((all_occurrences, mkVar id, pf_get_hyp_val gl id), Anonymous)) 
+    hyps 
+  in tclTHEN (generalize_gen_let lconstr) (clear hyps) gl
 
 (* Faudra-t-il une version avec plusieurs args de generalize_dep ?
-Cela peut-être troublant de faire "Generalize Dependent H n" dans
-"n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la
-généralisation dépendante par n.
+Cela peut-être troublant de faire "Generalize Dependent H n" dans
+"n:nat; H:n=n |- P(n)" et d'échouer parce que H a disparu après la
+généralisation dépendante par n.
 
 let quantify lconstr =
  List.fold_right
@@ -1487,9 +1499,9 @@ let quantify lconstr =
    tclIDTAC
 *)
 
-(* A dependent cut rule à la sequent calculus
+(* A dependent cut rule à la sequent calculus
    ------------------------------------------
-   Sera simplifiable le jour où il y aura un let in primitif dans constr
+   Sera simplifiable le jour où il y aura un let in primitif dans constr
 
    [letin_tac b na c (occ_hyp,occ_ccl) gl] transforms
    [...x1:T1(c),...,x2:T2(c),... |- G(c)] into
@@ -1816,11 +1828,11 @@ let induct_discharge destopt avoid' tac (avoid,ra) names gl =
   in
   peel_tac ra names no_move 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
+(* - 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
      substitutions aussi sur l'argument voisin *)
 
-(* Marche pas... faut prendre en compte l'occurrence précise... *)
+(* Marche pas... faut prendre en compte l'occurrence précise... *)
 
 let atomize_param_of_ind (indref,nparams,_) hyp0 gl =
   let tmptyp0 = pf_get_hyp_typ gl hyp0 in
@@ -1828,7 +1840,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 gl =
   let prods, indtyp = decompose_prod typ0 in
   let argl = snd (decompose_app indtyp) in
   let params = list_firstn nparams argl in
-  (* le gl est important pour ne pas préévaluer *)
+  (* le gl est important pour ne pas préévaluer *)
   let rec atomize_one i avoid gl =
     if i<>nparams then
       let tmptyp0 = pf_get_hyp_typ gl hyp0 in
@@ -2116,31 +2128,25 @@ let error_ind_scheme s =
   let s = if s <> "" then s^" " else s in
   error ("Cannot recognize "^s^"an induction scheme.")
 
-let mkEq t x y =
-  mkApp (build_coq_eq (), [| t; x; y |])
+let coq_eq = Lazy.lazy_from_fun Coqlib.build_coq_eq
+let coq_eq_refl = lazy ((Coqlib.build_coq_eq_data ()).Coqlib.refl)
 
-let mkRefl t x =
-  mkApp ((build_coq_eq_data ()).refl, [| t; x |])
+let coq_heq = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq")
+let coq_heq_refl = lazy (Coqlib.coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl")
 
-let mkHEq t x u y =
-  mkApp (coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq",
-	[| t; x; u; y |])
+let mkEq t x y = 
+  mkApp (Lazy.force coq_eq, [| refresh_universes_strict t; x; y |])
+    
+let mkRefl t x = 
+  mkApp (Lazy.force coq_eq_refl, [| refresh_universes_strict t; x |])
 
+let mkHEq t x u y =
+  mkApp (Lazy.force coq_heq,
+	[| refresh_universes_strict t; x; refresh_universes_strict u; y |])
+    
 let mkHRefl t x =
-  mkApp (coq_constant "mkHEq" ["Logic";"JMeq"] "JMeq_refl",
-	[| t; x |])
-
-(* let id = lazy (coq_constant "mkHEq" ["Init";"Datatypes"] "id") *)
-
-(* let mkHEq t x u y =  *)
-(*   let ty = new_Type () in *)
-(*   mkApp (coq_constant "mkHEq" ["Logic";"EqdepFacts"] "eq_dep", *)
-(* 	[| ty; mkApp (Lazy.force id, [|ty|]); t; x; u; y |]) *)
-
-(* let mkHRefl t x =  *)
-(*   let ty = new_Type () in *)
-(*   mkApp (coq_constant "mkHEq" ["Logic";"EqdepFacts"] "eq_dep_intro", *)
-(* 	[| ty; mkApp (Lazy.force id, [|ty|]); t; x |]) *)
+  mkApp (Lazy.force coq_heq_refl,
+	[| refresh_universes_strict t; x |])
 
 let lift_togethern n l =
   let l', _ =
@@ -2157,8 +2163,8 @@ let lift_list l = List.map (lift 1) l
 let ids_of_constr vars c =
   let rec aux vars c =
     match kind_of_term c with
-    | Var id -> if List.mem id vars then vars else id :: vars
-    | App (f, args) ->
+    | Var id -> Idset.add id vars
+    | App (f, args) -> 
 	(match kind_of_term f with
 	| Construct (ind,_)
 	| Ind ind ->
@@ -2168,6 +2174,16 @@ let ids_of_constr vars c =
 	| _ -> fold_constr aux vars c)
     | _ -> fold_constr aux vars c
   in aux vars c
+    
+let decompose_indapp f args =
+  match kind_of_term f with
+  | Construct (ind,_) 
+  | Ind ind ->
+      let (mib,mip) = Global.lookup_inductive ind in
+      let first = mib.Declarations.mind_nparams_rec in
+      let pars, args = array_chop first args in
+	mkApp (f, pars), args
+  | _ -> f, args
 
 let mk_term_eq env sigma ty t ty' t' =
   if Reductionops.is_conv env sigma ty ty' then
@@ -2203,24 +2219,52 @@ let make_abstract_generalize gl id concl dep ctx c eqs args refls =
   let appeqs = mkApp (instc, Array.of_list refls) in
     (* Finaly, apply the reflexivity proof for the original hyp, to get a term of type gl again. *)
     mkApp (appeqs, abshypt)
-
-let abstract_args gl id =
+      
+let deps_of_var id env =
+  Environ.fold_named_context
+    (fun _ (n,b,t) (acc : Idset.t) -> 
+      if Option.cata (occur_var env id) false b || occur_var env id t then
+	Idset.add n acc
+      else acc)
+    env ~init:Idset.empty
+    
+let idset_of_list =
+  List.fold_left (fun s x -> Idset.add x s) Idset.empty
+
+let hyps_of_vars env sign nogen hyps =
+  if Idset.is_empty hyps then [] 
+  else
+    let (_,lh) =
+      Sign.fold_named_context_reverse
+        (fun (hs,hl) (x,_,_ as d) ->
+	  if Idset.mem x nogen then (hs,hl)
+	  else if Idset.mem x hs then (hs,x::hl)
+	  else
+	    let xvars = global_vars_set_of_decl env d in
+	      if not (Idset.equal (Idset.diff xvars hs) Idset.empty) then
+		(Idset.add x hs, x :: hl)
+	      else (hs, hl))
+        ~init:(hyps,[])
+        sign 
+    in lh
+
+let abstract_args gl generalize_vars dep id = 
   let c = pf_get_hyp_typ gl id in
   let sigma = project gl in
   let env = pf_env gl in
   let concl = pf_concl gl in
-  let dep = dependent (mkVar id) concl in
+  let dep = dep || dependent (mkVar id) concl in
   let avoid = ref [] in
   let get_id name =
     let id = fresh_id !avoid (match name with Name n -> n | Anonymous -> id_of_string "gen_x") gl in
       avoid := id :: !avoid; id
   in
-  match kind_of_term c with
-      App (f, args) ->
+    match kind_of_term c with
+    | App (f, args) -> 
 	(* Build application generalized w.r.t. the argument plus the necessary eqs.
 	   From env |- c : forall G, T and args : G we build
 	   (T[G'], G' : ctx, env ; G' |- args' : G, eqs := G'_i = G_i, refls : G' = G, vars to generalize)
-
+	   
 	   eqs are not lifted w.r.t. each other yet. (* will be needed when going to dependent indexes *)
 	*)
 	let aux (prod, ctx, ctxenv, c, args, eqs, refls, vars, env) arg =
@@ -2232,8 +2276,9 @@ let abstract_args gl id =
 	  let liftargty = lift (List.length ctx) argty in
 	  let convertible = Reductionops.is_conv_leq ctxenv sigma liftargty ty in
 	    match kind_of_term arg with
-(* 	    | Var _ | Rel _ | Ind _ when convertible ->  *)
-(* 		(subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, vars, env) *)
+(* 	    | Var id -> *)
+(* 		let deps = deps_of_var id env in *)
+(* 		  (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, Idset.union deps vars, env) *)
 	    | _ ->
 		let name = get_id name in
 		let decl = (Name name, None, ty) in
@@ -2249,53 +2294,109 @@ let abstract_args gl id =
 		in
 		let eqs = eq :: lift_list eqs in
 		let refls = refl :: refls in
-		let vars = ids_of_constr vars arg in
-		  (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, vars, env)
+		let argvars = ids_of_constr vars arg in
+		  (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, Idset.union argvars vars, env)
+	in 
+	let f', args' = decompose_indapp f args in
+	let dogen, f', args' =
+	  if not (array_distinct args) then true, f', args'
+	  else
+	    match array_find_i (fun i x -> not (isVar x)) args' with
+	    | None -> false, f', args'
+	    | Some nonvar ->
+		let before, after = array_chop nonvar args' in
+		  true, mkApp (f', before), after
 	in
-	let f, args =
-	  match kind_of_term f with
-	  | Construct (ind,_)
-	  | Ind ind ->
-              let (mib,mip) = Global.lookup_inductive ind in
-	      let first = mib.Declarations.mind_nparams in
-	      let pars, args = array_chop first args in
-		mkApp (f, pars), args
-	  | _ -> f, args
-	in
-	  (match args with [||] -> None
-	  | _ ->
-	      let arity, ctx, ctxenv, c', args, eqs, refls, vars, env =
-		Array.fold_left aux (pf_type_of gl f,[],env,f,[],[],[],[],env) args
-	      in
-	      let args, refls = List.rev args, List.rev refls in
-		Some (make_abstract_generalize gl id concl dep ctx c' eqs args refls,
-		     dep, succ (List.length ctx), vars))
+	  if dogen then
+	    let arity, ctx, ctxenv, c', args, eqs, refls, vars, env = 
+	      Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Idset.empty,env) args'
+	    in
+	    let args, refls = List.rev args, List.rev refls in
+	    let vars = 
+	      if generalize_vars then
+		let nogen = Idset.add id Idset.empty in
+		  hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars
+	      else []
+	    in
+	      Some (make_abstract_generalize gl id concl dep ctx c' eqs args refls,
+		   dep, succ (List.length ctx), vars)
+	  else None
     | _ -> None
 
-let abstract_generalize id ?(generalize_vars=true) gl =
+let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id gl =
   Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
   let oldid = pf_get_new_id id gl in
-  let newc = abstract_args gl id in
+  let newc = abstract_args gl generalize_vars force_dep id in
     match newc with
-      | None -> tclIDTAC gl
-      | Some (newc, dep, n, vars) ->
-	  let tac =
-	    if dep then
-	      tclTHENLIST [refine newc; rename_hyp [(id, oldid)]; tclDO n intro;
-			   generalize_dep (mkVar oldid)]
-	    else
-	      tclTHENLIST [refine newc; clear [id]; tclDO n intro]
-	  in
-	    if generalize_vars then tclTHEN tac
-	      (tclFIRST [revert (List.rev vars) ;
-			 tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars]) gl
-	    else tac gl
+    | None -> tclIDTAC gl
+    | Some (newc, dep, n, vars) -> 
+	let tac =
+	  if dep then
+	    tclTHENLIST [refine newc; rename_hyp [(id, oldid)]; tclDO n intro; 
+			 generalize_dep (mkVar oldid)]	      
+	  else
+	    tclTHENLIST [refine newc; clear [id]; tclDO n intro]
+	in 
+	  if vars = [] then tac gl
+	  else tclTHEN tac 
+	    (fun gl -> tclFIRST [revert vars ;
+				 tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars] gl) gl
+
+let specialize_hypothesis id gl =
+  let env = pf_env gl in
+  let ty = pf_get_hyp_typ gl id in
+  let evars = ref (create_evar_defs (project gl)) in
+  let unif env evars c1 c2 = Evarconv.e_conv env evars c2 c1 in
+  let rec aux in_eqs ctx acc ty =
+    match kind_of_term ty with
+    | Prod (na, t, b) -> 
+	(match kind_of_term t with
+	| App (eq, [| eqty; x; y |]) when eq_constr eq (Lazy.force coq_eq) ->
+	    let c = if noccur_between 1 (List.length ctx) x then y else x in
+	    let pt = mkApp (Lazy.force coq_eq, [| eqty; c; c |]) in
+	    let p = mkApp (Lazy.force coq_eq_refl, [| eqty; c |]) in
+	      if unif (push_rel_context ctx env) evars pt t then
+		aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
+	      else acc, in_eqs, ctx, ty
+	| App (heq, [| eqty; x; eqty'; y |]) when eq_constr heq (Lazy.force coq_heq) ->
+	    let eqt, c = if noccur_between 1 (List.length ctx) x then eqty', y else eqty, x in
+	    let pt = mkApp (Lazy.force coq_heq, [| eqt; c; eqt; c |]) in
+	    let p = mkApp (Lazy.force coq_heq_refl, [| eqt; c |]) in
+	      if unif (push_rel_context ctx env) evars pt t then
+		aux true ctx (mkApp (acc, [| p |])) (subst1 p b)
+	      else acc, in_eqs, ctx, ty
+	| _ -> 
+	    if in_eqs then acc, in_eqs, ctx, ty
+	    else 
+	      let e = e_new_evar evars (push_rel_context ctx env) t in
+		aux false ((na, Some e, t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
+    | t -> acc, in_eqs, ctx, ty
+  in 
+  let acc, worked, ctx, ty = aux false [] (mkVar id) ty in
+  let ctx' = nf_rel_context_evar !evars ctx in
+  let ctx'' = List.map (fun (n,b,t as decl) ->
+    match b with
+    | Some k when isEvar k -> (n,None,t)
+    | b -> decl) ctx'
+  in
+  let ty' = it_mkProd_or_LetIn ty ctx'' in
+  let acc' = it_mkLambda_or_LetIn acc ctx'' in
+  let ty' = Tacred.whd_simpl env !evars ty' 
+  and acc' = Tacred.whd_simpl env !evars acc' in
+  let ty' = Evarutil.nf_isevar !evars ty' in
+    if worked then
+      tclTHENFIRST (Tacmach.internal_cut true id ty')
+	(exact_no_check (refresh_universes_strict acc')) gl
+    else tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) gl
+      
 
 let dependent_pattern c gl =
   let cty = pf_type_of gl c in
   let deps =
     match kind_of_term cty with
-    | App (f, args) -> Array.to_list args
+    | App (f, args) -> 
+	let f', args' = decompose_indapp f args in 
+	  Array.to_list args'
     | _ -> []
   in
   let varname c = match kind_of_term c with
@@ -2500,7 +2601,7 @@ let compute_elim_sig ?elimc elimt =
 
 let compute_scheme_signature scheme names_info ind_type_guess =
   let f,l = decompose_app scheme.concl in
-  (* Vérifier que les arguments de Qi sont bien les xi. *)
+  (* Vérifier que les arguments de Qi sont bien les xi. *)
   match scheme.indarg with
     | Some (_,Some _,_) -> error "Strange letin, cannot recognize an induction scheme."
     | None -> (* Non standard scheme *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index cedcbf7caa..7d65ab7525 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -375,7 +375,8 @@ val tclABSTRACT : identifier option -> tactic -> tactic
 
 val admit_as_an_axiom : tactic
 
-val abstract_generalize : identifier -> ?generalize_vars:bool -> tactic
+val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> identifier -> tactic
+val specialize_hypothesis : identifier -> tactic
 
 val dependent_pattern : constr -> tactic