Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

39 files changed, 485 insertions, 452 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 45052685..46274f83 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -359,8 +359,7 @@ and my_find_search_delta db_list local_db hdc concl =
       	(local_db::db_list)
 
 and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly})) =
-  let tactic = 
-    match t with
+  let tactic = function
     | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
     | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf")
     | Give_exact (c, cl)  -> exact poly (c, cl)
@@ -378,7 +377,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly}))
     | Extern tacast -> 
       conclPattern concl p tacast
   in
-  tclLOG dbg (fun () -> pr_autotactic t) tactic
+  tclLOG dbg (fun () -> pr_autotactic t) (run_auto_tactic t tactic)
 
 and trivial_resolve dbg mod_delta db_list local_db cl =
   try
diff --git a/tactics/auto.mli b/tactics/auto.mli
index ea3f0ac0..0cc8a0b1 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Proof_type
 open Clenv
 open Pattern
 open Evd
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index ee8e1855..4eb8a792 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -211,6 +211,7 @@ let cache_hintrewrite (_,(rbase,lrl)) =
   let base = try raw_find_base rbase with Not_found -> HintDN.empty in
   let max = try fst (Util.List.last (HintDN.find_all base)) with Failure _ -> 0
   in
+  let lrl = HintDN.refresh_metas lrl in
   let lrl = HintDN.map (fun (i,h) -> (i + max, h)) lrl in
     rewtab:=String.Map.add rbase (HintDN.union lrl base) !rewtab
 
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 1f5177c3..b87d6575 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -144,7 +144,7 @@ struct
 
  type t = Dn.t
 
-  let create = Dn.create
+  let empty = Dn.empty
 
   let add = function
     | None ->
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 6c396b4c..f29d1861 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -28,7 +28,7 @@ module Make :
 sig
   type t
 
-  val create : unit ->  t
+  val empty : t
 
   val add : transparent_state option -> t -> (constr_pattern * Z.t) -> t
   val rmv : transparent_state option -> t -> (constr_pattern * Z.t) -> t
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 1c15fa40..e11458c0 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -17,7 +17,6 @@ open Proof_type
 open Tacticals
 open Tacmach
 open Tactics
-open Patternops
 open Clenv
 open Typeclasses
 open Globnames
@@ -42,7 +41,7 @@ let get_typeclasses_dependency_order () = !typeclasses_dependency_order
 
 open Goptions
 
-let set_typeclasses_modulo_eta =
+let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
@@ -51,7 +50,7 @@ let set_typeclasses_modulo_eta =
       optread  = get_typeclasses_modulo_eta;
       optwrite = set_typeclasses_modulo_eta; }
 
-let set_typeclasses_dependency_order =
+let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
@@ -222,20 +221,19 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
   in
   let tac_of_hint =
     fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) ->
-      let tac =
-	match t with
-	  | Res_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_resolve poly flags)
-	  | ERes_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_e_resolve poly flags)
-	  | Give_exact c -> e_give_exact flags poly c
-	  | Res_pf_THEN_trivial_fail (term,cl) ->
-              tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
-	        (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)
-	  | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c])
-	  | Extern tacast ->
-	    Proofview.V82.of_tactic (conclPattern concl p tacast)
+      let tac = function
+      | Res_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_resolve poly flags))
+      | ERes_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
+      | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c)
+      | Res_pf_THEN_trivial_fail (term,cl) ->
+          Proofview.V82.tactic (tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
+            (if complete then tclIDTAC else e_trivial_fail_db db_list local_db))
+      | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c]))
+      | Extern tacast -> conclPattern concl p tacast
       in
+      let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in
       let tac = if complete then tclCOMPLETE tac else tac in
-	match t with
+	match repr_auto_tactic t with
 	| Extern _ -> (tac,b,true, name, lazy (pr_autotactic t))
 	| _ ->
 (* 	  let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *)
@@ -351,7 +349,9 @@ let make_autogoal_hints =
       let sign = pf_filtered_hyps g in
       let (onlyc, sign', cached_hints) = !cache in
 	if onlyc == only_classes && 
-	  (sign == sign' || Environ.eq_named_context_val sign sign') then
+	  (sign == sign' || Environ.eq_named_context_val sign sign') 
+	  && Hint_db.transparent_state cached_hints == st
+	then
 	  cached_hints
 	else
 	  let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 9ee14b80..9b69481d 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -9,8 +9,6 @@
 open Errors
 open Term
 open Hipattern
-open Tacmach
-open Tacticals
 open Tactics
 open Coqlib
 open Reductionops
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 5c039e72..e909a14c 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -71,14 +71,14 @@ END
 TACTIC EXTEND left_with
   [ "left" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Proofview.Unsafe.tclEVARS sigma <*> Tactics.left_with_bindings false bl
+    Tacticals.New.tclWITHHOLES false (Tactics.left_with_bindings false bl) sigma
   ]
 END
 
 TACTIC EXTEND eleft_with
   [ "eleft" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Tacticals.New.tclWITHHOLES true (Tactics.left_with_bindings true) sigma bl
+    Tacticals.New.tclWITHHOLES true (Tactics.left_with_bindings true bl) sigma
   ]
 END
 
@@ -95,14 +95,14 @@ END
 TACTIC EXTEND right_with
   [ "right" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Proofview.Unsafe.tclEVARS sigma <*> Tactics.right_with_bindings false bl
+    Tacticals.New.tclWITHHOLES false (Tactics.right_with_bindings false bl) sigma
   ]
 END
 
 TACTIC EXTEND eright_with
   [ "eright" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Tacticals.New.tclWITHHOLES true (Tactics.right_with_bindings true) sigma bl
+    Tacticals.New.tclWITHHOLES true (Tactics.right_with_bindings true bl) sigma
   ]
 END
 
@@ -117,8 +117,8 @@ TACTIC EXTEND constructor
 | [ "constructor" int_or_var(i) "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma; it = bl } = bl in
     let i = Tacinterp.interp_int_or_var ist i in
-    let tac c = Tactics.constructor_tac false None i c in
-    Proofview.Unsafe.tclEVARS sigma <*> tac bl
+    let tac = Tactics.constructor_tac false None i bl in
+    Tacticals.New.tclWITHHOLES false tac sigma
   ]
 END
 
@@ -131,8 +131,8 @@ TACTIC EXTEND econstructor
 | [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma; it = bl } = bl in
     let i = Tacinterp.interp_int_or_var ist i in
-    let tac c = Tactics.constructor_tac true None i c in
-    Tacticals.New.tclWITHHOLES true tac sigma bl
+    let tac = Tactics.constructor_tac true None i bl in
+    Tacticals.New.tclWITHHOLES true tac sigma
   ]
 END
 
@@ -141,8 +141,8 @@ END
 TACTIC EXTEND specialize
   [ "specialize" constr_with_bindings(c) ] -> [
     let { Evd.sigma = sigma; it = c } = c in
-    let specialize c = Proofview.V82.tactic (Tactics.specialize c) in
-    Proofview.Unsafe.tclEVARS sigma <*> specialize c
+    let specialize = Proofview.V82.tactic (Tactics.specialize c) in
+    Tacticals.New.tclWITHHOLES false specialize sigma
   ]
 END
 
@@ -163,14 +163,14 @@ END
 TACTIC EXTEND split_with
   [ "split" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Proofview.Unsafe.tclEVARS sigma <*> Tactics.split_with_bindings false [bl]
+    Tacticals.New.tclWITHHOLES false (Tactics.split_with_bindings false [bl]) sigma
   ]
 END
 
 TACTIC EXTEND esplit_with
   [ "esplit" "with" bindings(bl) ] -> [
     let { Evd.sigma = sigma ; it = bl } = bl in
-    Tacticals.New.tclWITHHOLES true (Tactics.split_with_bindings true) sigma [bl]
+    Tacticals.New.tclWITHHOLES true (Tactics.split_with_bindings true [bl]) sigma
   ]
 END
 
@@ -196,6 +196,12 @@ TACTIC EXTEND simple_destruct
   [ "simple" "destruct" quantified_hypothesis(h) ] -> [ Tactics.simple_destruct h ]
 END
 
+(* Admit *)
+
+TACTIC EXTEND admit
+ [ "admit" ] -> [ Proofview.give_up ]
+END
+
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 
 open Tacexpr
diff --git a/tactics/dn.ml b/tactics/dn.ml
index 3b1614d6..aed2c283 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -38,7 +38,7 @@ struct
 
   type  t = Trie.t
 
-  let create () = Trie.empty
+  let empty = Trie.empty
 
 (* [path_of dna pat] returns the list of nodes of the pattern [pat] read in
 prefix ordering, [dna] is the function returning the main node of a pattern *)
diff --git a/tactics/dn.mli b/tactics/dn.mli
index 20407e9d..2a60c3eb 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.mli
@@ -10,7 +10,7 @@ sig
 
   type t
 
-  val create : unit -> t
+  val empty : t
 
   (** [add t f (tree,inf)] adds a structured object [tree] together with
      the associated information [inf] to the table [t]; the function
diff --git a/tactics/dnet.ml b/tactics/dnet.ml
index 61a35866..93334db7 100644
--- a/tactics/dnet.ml
+++ b/tactics/dnet.ml
@@ -39,6 +39,7 @@ sig
   val inter : t -> t -> t
   val union : t -> t -> t
   val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t
+  val map_metas : (meta -> meta) -> t -> t
 end
 
 module Make =
@@ -121,7 +122,7 @@ struct
 	     Idset.union acc s2
 	 ) t Idset.empty)
 
-(*   (\* optimization hack: Not_found is catched in fold_pattern *\) *)
+(*   (\* optimization hack: Not_found is caught in fold_pattern *\) *)
 (*   let fast_inter s1 s2 = *)
 (*     if Idset.is_empty s1 || Idset.is_empty s2 then raise Not_found *)
 (*     else Idset.inter s1 s2 *)
@@ -176,7 +177,7 @@ struct
     let is_empty : t -> bool = function 
       | None -> false
       | Some s -> S.is_empty s
-    (* optimization hack: Not_found is catched in fold_pattern *)
+    (* optimization hack: Not_found is caught in fold_pattern *)
     let fast_inter s1 s2 =
       if is_empty s1 || is_empty s2 then raise Not_found
       else let r = inter s1 s2 in 
@@ -288,4 +289,13 @@ struct
       | Node e -> Node (T.map (map sidset sterm) e) in
     Nodes (tmap_map sterm snode t, Mmap.map (idset_map sidset) m)
 
+  let rec map_metas f (Nodes (t, m)) : t =
+    let f_node = function
+      | Terminal (e, is) -> Terminal (T.map (map_metas f) e, is)
+      | Node e -> Node (T.map (map_metas f) e)
+    in
+    let m' = Mmap.fold (fun m s acc -> Mmap.add (f m) s acc) m Mmap.empty in
+    let t' = Tmap.fold (fun k n acc -> Tmap.add k (f_node n) acc) t Tmap.empty in
+    Nodes (t', m')
+
 end
diff --git a/tactics/dnet.mli b/tactics/dnet.mli
index 4bfa7263..52853d70 100644
--- a/tactics/dnet.mli
+++ b/tactics/dnet.mli
@@ -113,6 +113,8 @@ sig
 
   (** apply a function on each identifier and node of terms in a dnet *)
   val map : (ident -> ident) -> (unit structure -> unit structure) -> t -> t
+
+  val map_metas : (meta -> meta) -> t -> t
 end
 
 module Make :
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 30c5e686..27c3569d 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -125,6 +125,14 @@ let unify_e_resolve poly flags (c,clenv) gls =
     tclTHEN (Refiner.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
       (Proofview.V82.of_tactic (Tactics.Simple.eapply (Vars.subst_univs_level_constr subst c))) gls
 
+let hintmap_of hdc concl =
+  match hdc with
+  | None -> fun db -> Hint_db.map_none db
+  | Some hdc ->
+    if occur_existential concl then (fun db -> Hint_db.map_existential hdc concl db)
+    else (fun db -> Hint_db.map_auto hdc concl db)
+   (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
+
 let e_exact poly flags (c,clenv) =
   let clenv', subst = 
     if poly then Clenv.refresh_undefined_univs clenv 
@@ -145,47 +153,39 @@ let rec e_trivial_fail_db db_list local_db goal =
     tclFIRST (List.map tclCOMPLETE tacl) goal
 
 and e_my_find_search db_list local_db hdc concl =
+  let hint_of_db = hintmap_of hdc concl in
   let hintl =
-    if occur_existential concl then
-      List.map_append (fun db ->
-	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
-	  List.map (fun x -> flags, x) (Hint_db.map_existential hdc concl db)
-   (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)) (local_db::db_list)
-    else
       List.map_append (fun db ->
 	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
-	  List.map (fun x -> flags, x) (Hint_db.map_auto hdc concl db)) (local_db::db_list)
+	  List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list)
   in
   let tac_of_hint =
     fun (st, {pri = b; pat = p; code = t; poly = poly}) ->
       (b,
-       let tac =
-	 match t with
-	   | Res_pf (term,cl) -> Proofview.V82.of_tactic (unify_resolve poly st (term,cl))
-	   | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
-	   | Give_exact (c,cl) -> e_exact poly st (c,cl)
-	   | Res_pf_THEN_trivial_fail (term,cl) ->
-               tclTHEN (unify_e_resolve poly st (term,cl))
-		 (e_trivial_fail_db db_list local_db)
-	   | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
-	   | Extern tacast -> Proofview.V82.of_tactic (conclPattern concl p tacast)
+        let tac = function
+        | Res_pf (term,cl) -> unify_resolve poly st (term,cl)
+        | ERes_pf (term,cl) -> Proofview.V82.tactic (unify_e_resolve poly st (term,cl))
+        | Give_exact (c,cl) -> Proofview.V82.tactic (e_exact poly st (c,cl))
+        | Res_pf_THEN_trivial_fail (term,cl) ->
+          Proofview.V82.tactic (tclTHEN (unify_e_resolve poly st (term,cl))
+            (e_trivial_fail_db db_list local_db))
+        | Unfold_nth c -> Proofview.V82.tactic (reduce (Unfold [AllOccurrences,c]) onConcl)
+        | Extern tacast -> conclPattern concl p tacast
        in
-       (tac,lazy (pr_autotactic t)))
+       let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in
+       (tac, lazy (pr_autotactic t)))
   in
   List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db gl =
-  try
-    priority
-      (e_my_find_search db_list local_db
-	 (decompose_app_bound gl) gl)
-  with Bound | Not_found -> []
+  let hd = try Some (decompose_app_bound gl) with Bound -> None in
+  try priority (e_my_find_search db_list local_db hd gl)
+  with Not_found -> []
 
 let e_possible_resolve db_list local_db gl =
-  try List.map snd
-    (e_my_find_search db_list local_db
-	(decompose_app_bound gl) gl)
-  with Bound | Not_found -> []
+  let hd = try Some (decompose_app_bound gl) with Bound -> None in
+  try List.map (fun (b, (tac, pp)) -> (tac, b, pp)) (e_my_find_search db_list local_db hd gl)
+  with Not_found -> []
 
 let find_first_goal gls =
   try first_goal gls with UserError _ -> assert false
@@ -194,6 +194,7 @@ let find_first_goal gls =
     exploration functor [Explore.Make]. *)
 
 type search_state = {
+  priority : int;
   depth : int; (*r depth of search before failing *)
   tacres : goal list sigma;
   last_tactic : std_ppcmds Lazy.t;
@@ -221,12 +222,12 @@ module SearchProblem = struct
 (*     msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *)
     let rec aux = function
       | [] -> []
-      | (tac,pptac) :: tacl ->
+      | (tac, cost, pptac) :: tacl ->
 	  try
 	    let lgls = apply_tac_list tac glls in
 (* 	    let gl = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
 (* 	      msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
-	      (lgls,pptac) :: aux tacl
+	      (lgls, cost, pptac) :: aux tacl
 	  with e when Errors.noncritical e ->
             let e = Errors.push e in
             Refiner.catch_failerror e; aux tacl
@@ -236,8 +237,11 @@ module SearchProblem = struct
      number of remaining goals. *)
   let compare s s' =
     let d = s'.depth - s.depth in
+    let d' = Int.compare s.priority s'.priority in
     let nbgoals s = List.length (sig_it s.tacres) in
-    if not (Int.equal d 0) then d else nbgoals s - nbgoals s'
+    if not (Int.equal d' 0) then d'
+    else if not (Int.equal d 0) then d
+    else Int.compare (nbgoals s) (nbgoals s')
 
   let branching s =
     if Int.equal s.depth 0 then
@@ -248,42 +252,39 @@ module SearchProblem = struct
       let nbgl = List.length (sig_it lg) in
       assert (nbgl > 0);
       let g = find_first_goal lg in
+      let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in
       let assumption_tacs =
-	let l =
-	  filter_tactics s.tacres
-	    (List.map
-	       (fun id -> (e_give_exact (mkVar id),
-			   lazy (str "exact" ++ spc () ++ pr_id id)))
-	       (pf_ids_of_hyps g))
-	in
-	List.map (fun (res,pp) -> { depth = s.depth; tacres = res;
+        let tacs = List.map map_assum (pf_ids_of_hyps g) in
+        let l = filter_tactics s.tacres tacs in
+	List.map (fun (res, cost, pp) -> { depth = s.depth; priority = cost; tacres = res;
 				    last_tactic = pp; dblist = s.dblist;
 				    localdb = List.tl s.localdb;
 				    prev = ps}) l
       in
       let intro_tac =
+        let l = filter_tactics s.tacres [Proofview.V82.of_tactic Tactics.intro, (-1), lazy (str "intro")] in
 	List.map
-	  (fun (lgls as res,pp) ->
+	  (fun (lgls, cost, pp) ->
 	     let g' = first_goal lgls in
 	     let hintl =
 	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
 	     in
              let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
-	     { depth = s.depth; tacres = res;
+	     { depth = s.depth; priority = cost; tacres = lgls;
 	       last_tactic = pp; dblist = s.dblist;
 	       localdb = ldb :: List.tl s.localdb; prev = ps })
-	  (filter_tactics s.tacres [Proofview.V82.of_tactic Tactics.intro,lazy (str "intro")])
+	  l
       in
       let rec_tacs =
 	let l =
 	  filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
 	in
 	List.map
-	  (fun (lgls as res, pp) ->
+	  (fun (lgls, cost, pp) ->
 	     let nbgl' = List.length (sig_it lgls) in
 	     if nbgl' < nbgl then
-	       { depth = s.depth; tacres = res; last_tactic = pp; prev = ps;
-		 dblist = s.dblist; localdb = List.tl s.localdb }
+	       { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp;
+                  prev = ps; dblist = s.dblist; localdb = List.tl s.localdb }
 	     else
 	       let newlocal = 
 		 let hyps = pf_hyps g in
@@ -294,7 +295,7 @@ module SearchProblem = struct
 		       else make_local_hint_db (pf_env gls) (project gls) ~ts:full_transparent_state true [])
 		     (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls))
 	       in
-		 { depth = pred s.depth; tacres = res;
+		 { depth = pred s.depth; priority = cost; tacres = lgls;
 		   dblist = s.dblist; last_tactic = pp; prev = ps;
 		   localdb = newlocal @ List.tl s.localdb })
 	  l
@@ -363,6 +364,7 @@ let pr_info dbg s =
 
 let make_initial_state dbg n gl dblist localdb =
   { depth = n;
+    priority = 0;
     tacres = tclIDTAC gl;
     last_tactic = lazy (mt());
     dblist = dblist;
@@ -566,7 +568,7 @@ let autounfold_one db cl =
   in
     if did then
       match cl with
-      | Some hyp -> change_in_hyp None (fun sigma -> sigma, c') hyp
+      | Some hyp -> change_in_hyp None (make_change_arg c') hyp
       | None -> convert_concl_no_check c' DEFAULTcast
     else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
   end
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 19e2f198..7073e8a2 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -8,7 +8,6 @@
 
 open Term
 open Proof_type
-open Auto
 open Evd
 open Hints
 
diff --git a/tactics/elim.ml b/tactics/elim.ml
index b7d5b102..3cb4fa9c 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -15,7 +15,6 @@ open Hipattern
 open Tacmach.New
 open Tacticals.New
 open Tactics
-open Misctypes
 open Proofview.Notations
 
 let introElimAssumsThen tac ba =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c130fa15..7ab8d0c3 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -487,9 +487,6 @@ let apply_special_clear_request clear_flag f =
       e when catchable_exception e -> tclIDTAC
   end
 
-type delayed_open_constr_with_bindings =
-    env -> evar_map -> evar_map * constr with_bindings
-
 let general_multi_rewrite with_evars l cl tac =
   let do1 l2r f =
     Proofview.Goal.enter begin fun gl ->
@@ -497,7 +494,7 @@ let general_multi_rewrite with_evars l cl tac =
       let env = Proofview.Goal.env gl in
       let sigma,c = f env sigma in
       tclWITHHOLES with_evars
-        (general_rewrite_clause l2r with_evars ?tac c) sigma cl
+        (general_rewrite_clause l2r with_evars ?tac c cl) sigma
     end
   in
   let rec doN l2r c = function
@@ -1233,8 +1230,6 @@ let try_delta_expand env sigma t =
 let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined")
 let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
 
-let eqdep_dec = qualid_of_string "Coq.Logic.Eqdep_dec"
-
 let inject_if_homogenous_dependent_pair ty =
   Proofview.Goal.nf_enter begin fun gl ->
   try
@@ -1257,7 +1252,7 @@ let inject_if_homogenous_dependent_pair ty =
     (* knows inductive types *)
     if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
       pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
-    Library.require_library [Loc.ghost,eqdep_dec] (Some false);
+    Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"];
     let new_eq_args = [|pf_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
       ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
@@ -1474,8 +1469,6 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
 (* then it uses the predicate "\x.phi(proj1_sig x,proj2_sig x)", and so   *)
 (* on for further iterated sigma-tuples                                   *)
 
-exception NothingToRewrite
-
 let cutSubstInConcl l2r eqn =
   Proofview.Goal.nf_enter begin fun gl ->
   let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
@@ -1500,10 +1493,10 @@ let cutSubstInHyp l2r eqn id =
   tclTHENFIRST
     (tclTHENLIST [
        (Proofview.Unsafe.tclEVARS sigma);
-       (change_in_hyp None (fun s -> s,typ) (id,InHypTypeOnly));
+       (change_in_hyp None (make_change_arg typ) (id,InHypTypeOnly));
        (replace_core (onHyp id) l2r eqn)
     ])
-    (change_in_hyp None (fun s -> s,expected) (id,InHypTypeOnly))
+    (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly))
   end
 
 let try_rewrite tac =
@@ -1513,9 +1506,6 @@ let try_rewrite tac =
     | e when catchable_exception e ->
 	tclZEROMSG
           (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
-    | NothingToRewrite ->
-	tclZEROMSG
-          (strbrk "Nothing to rewrite.")
     | e -> Proofview.tclZERO ~info e
   end
 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 90d8a224..3e13ee57 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -11,7 +11,6 @@ open Names
 open Term
 open Evd
 open Environ
-open Tacmach
 open Tacexpr
 open Ind_tables
 open Locus
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 2aafaf08..c3fe6b65 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -71,8 +71,11 @@ let let_evar name typ =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
-    let id = Namegen.id_of_name_using_hdchar env typ name in
-    let id = Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env)) in
+    let id = match name with
+    | Names.Anonymous -> 
+      let id = Namegen.id_of_name_using_hdchar env typ name in
+      Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env))
+    | Names.Name id -> id in
     let sigma',evar = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma'))
       (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere)
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index 42d00e1e..2c4df060 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Tacmach
 open Names
 open Tacexpr
 open Locus
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index f3482c31..891e2dba 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -21,26 +21,22 @@ open Util
 open Evd
 open Equality
 open Misctypes
-open Proofview.Notations
 
 DECLARE PLUGIN "extratactics"
 
 (**********************************************************************)
-(* admit, replace, discriminate, injection, simplify_eq               *)
+(* replace, discriminate, injection, simplify_eq                      *)
 (* cutrewrite, dependent rewrite                                      *)
 
-TACTIC EXTEND admit
-  [ "admit" ] -> [ admit_as_an_axiom ]
-END
-
-let replace_in_clause_maybe_by (sigma,c1) c2 cl  tac =
-  Proofview.Unsafe.tclEVARS sigma <*>
-    (replace_in_clause_maybe_by c1 c2 cl)
-    (Option.map Tacinterp.eval_tactic tac)
+let replace_in_clause_maybe_by (sigma1,c1) c2 cl  tac =
+  Tacticals.New.tclWITHHOLES false
+    (replace_in_clause_maybe_by c1 c2 cl (Option.map Tacinterp.eval_tactic tac))
+    sigma1
 
 let replace_term dir_opt (sigma,c) cl =
-  Proofview.Unsafe.tclEVARS sigma <*>
-    (replace_term dir_opt c) cl
+  Tacticals.New.tclWITHHOLES false
+    (replace_term dir_opt c cl)
+    sigma
 
 TACTIC EXTEND replace
    ["replace" open_constr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
@@ -71,8 +67,8 @@ let induction_arg_of_quantified_hyp = function
    ElimOnIdent and not as "constr" *)
 
 let elimOnConstrWithHoles tac with_evars c =
-  Tacticals.New.tclWITHHOLES with_evars (tac with_evars) 
-    c.sigma (Some (None,ElimOnConstr c.it))
+  Tacticals.New.tclWITHHOLES with_evars
+    (tac with_evars (Some (None,ElimOnConstr c.it))) c.sigma
 
 TACTIC EXTEND simplify_eq_main
 | [ "simplify_eq" constr_with_bindings(c) ] ->
@@ -202,7 +198,7 @@ END
 
 let onSomeWithHoles tac = function
   | None -> tac None
-  | Some c -> Proofview.Unsafe.tclEVARS c.sigma <*> tac (Some c.it)
+  | Some c -> Tacticals.New.tclWITHHOLES false (tac (Some c.it)) c.sigma
 
 TACTIC EXTEND contradiction
  [ "contradiction" constr_with_bindings_opt(c) ] ->
@@ -246,8 +242,8 @@ END
 
 let rewrite_star clause orient occs (sigma,c) (tac : glob_tactic_expr option) =
   let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in
-  Proofview.Unsafe.tclEVARS sigma <*>
-    general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true
+  Tacticals.New.tclWITHHOLES false
+    (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true) sigma
 
 TACTIC EXTEND rewrite_star
 | [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] ->
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 5621c365..55d62e15 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -68,7 +68,7 @@ let decompose_app_bound t =
 (*           The Type of Constructions Autotactic Hints                 *)
 (************************************************************************)
 
-type 'a auto_tactic =
+type 'a auto_tactic_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
   | Give_exact of 'a
@@ -92,18 +92,23 @@ type hint_term =
   | IsGlobRef of global_reference
   | IsConstr of constr * Univ.universe_context_set
 
+type 'a auto_tactic = 'a auto_tactic_ast
+
 type 'a gen_auto_tactic = {
   pri  : int;            (* A number lower is higher priority *)
   poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
   pat  : constr_pattern option; (* A pattern for the concl of the Goal *)
   name  : hints_path_atom; (* A potential name to refer to the hint *) 
-  code : 'a auto_tactic     (* the tactic to apply when the concl matches pat *)
+  code : 'a     (* the tactic to apply when the concl matches pat *)
 }
 
-type pri_auto_tactic = (constr * clausenv) gen_auto_tactic
+type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic
 
 type hint_entry = global_reference option * 
-  (constr * types * Univ.universe_context_set) gen_auto_tactic
+  (constr * types * Univ.universe_context_set) auto_tactic_ast gen_auto_tactic
+
+let run_auto_tactic tac k = k tac
+let repr_auto_tactic tac = tac
 
 let eq_hints_path_atom p1 p2 = match p1, p2 with
 | PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2
@@ -156,10 +161,19 @@ module Bounded_net = Btermdn.Make(struct
 				    let compare = pri_order_int
 				  end)
 
-type search_entry = stored_data list * stored_data list * Bounded_net.t * bool array list
-
+type search_entry = {
+  sentry_nopat : stored_data list;
+  sentry_pat : stored_data list;
+  sentry_bnet : Bounded_net.t;
+  sentry_mode : bool array list;
+}
 
-let empty_se = ([],[],Bounded_net.create (),[])
+let empty_se = {
+  sentry_nopat = [];
+  sentry_pat = [];
+  sentry_bnet = Bounded_net.empty;
+  sentry_mode = [];
+}
 
 let eq_pri_auto_tactic (_, x) (_, y) =
   if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then
@@ -177,27 +191,29 @@ let eq_pri_auto_tactic (_, x) (_, y) =
   else
     false
 
-let add_tac pat t st (l,l',dn,m) =
+let add_tac pat t st se =
   match pat with
   | None -> 
-    if not (List.exists (eq_pri_auto_tactic t) l) then (List.insert pri_order t l, l', dn, m) 
-    else (l, l', dn, m)
+    if List.exists (eq_pri_auto_tactic t) se.sentry_nopat then se
+    else { se with sentry_nopat = List.insert pri_order t se.sentry_nopat }
   | Some pat -> 
-    if not (List.exists (eq_pri_auto_tactic t) l')
-    then (l, List.insert pri_order t l', Bounded_net.add st dn (pat,t), m) else (l, l', dn, m)
+    if List.exists (eq_pri_auto_tactic t) se.sentry_pat then se
+    else { se with
+        sentry_pat = List.insert pri_order t se.sentry_pat;
+        sentry_bnet = Bounded_net.add st se.sentry_bnet (pat, t); }
 
-let rebuild_dn st ((l,l',dn,m) : search_entry) =
+let rebuild_dn st se =
   let dn' = 
     List.fold_left 
       (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t)))
-      (Bounded_net.create ()) l'
+      Bounded_net.empty se.sentry_pat
   in
-    (l, l', dn', m)
+  { se with sentry_bnet = dn' }
 
-let lookup_tacs concl st (l,l',dn) =
-  let l'  = Bounded_net.lookup st dn concl in
+let lookup_tacs concl st se =
+  let l'  = Bounded_net.lookup st se.sentry_bnet concl in
   let sl' = List.stable_sort pri_order_int l' in
-    List.merge pri_order_int l sl'
+  List.merge pri_order_int se.sentry_nopat sl'
 
 module Constr_map = Map.Make(RefOrdered)
 
@@ -378,7 +394,7 @@ module Hint_db = struct
     hintdb_state : Names.transparent_state;
     hintdb_cut : hints_path;
     hintdb_unfolds : Id.Set.t * Cset.t;
-    mutable hintdb_max_id : int;
+    hintdb_max_id : int;
     use_dn : bool;
     hintdb_map : search_entry Constr_map.t;
     (* A list of unindexed entries starting with an unfoldable constant
@@ -386,8 +402,9 @@ module Hint_db = struct
     hintdb_nopat : (global_reference option * stored_data) list
   }
 
-  let next_hint_id t = 
-    let h = t.hintdb_max_id in t.hintdb_max_id <- succ t.hintdb_max_id; h
+  let next_hint_id db =
+    let h = db.hintdb_max_id in
+    { db with hintdb_max_id = succ db.hintdb_max_id }, h
 
   let empty st use_dn = { hintdb_state = st;
 			  hintdb_cut = PathEmpty;
@@ -411,34 +428,38 @@ module Hint_db = struct
     if List.is_empty modes then true
     else List.exists (matches_mode args) modes
 
+  let merge_entry db nopat pat =
+    let h = Sort.merge pri_order (List.map snd db.hintdb_nopat @ nopat) pat in
+    List.map realize_tac h
+
   let map_none db =
-    List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat) [])
-    
+    merge_entry db [] []
+
   let map_all k db =
-    let (l,l',_,_) = find k db in
-      List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat @ l) l')
+    let se = find k db in
+    merge_entry db se.sentry_nopat se.sentry_pat
 	
   (** Precondition: concl has no existentials *)
   let map_auto (k,args) concl db =
-    let (l,l',dn,m) = find k db in
+    let se = find k db in
     let st = if db.use_dn then  (Some db.hintdb_state) else None in
-    let l' = lookup_tacs concl st (l,l',dn) in
-      List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat) l')
+    let pat = lookup_tacs concl st se in
+    merge_entry db [] pat
 
   let map_existential (k,args) concl db =
-    let (l,l',_,m) = find k db in
-      if matches_modes args m then
-	List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat @ l) l')
-      else List.map realize_tac (List.map snd db.hintdb_nopat)
+    let se = find k db in
+      if matches_modes args se.sentry_mode then
+        merge_entry db se.sentry_nopat se.sentry_pat
+      else merge_entry db [] []
 
   (* [c] contains an existential *)
   let map_eauto (k,args) concl db =
-    let (l,l',dn,m) = find k db in
-      if matches_modes args m then
-	let st = if db.use_dn then Some db.hintdb_state else None in
-	let l' = lookup_tacs concl st (l,l',dn) in
-	  List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat) l')
-      else List.map realize_tac (List.map snd db.hintdb_nopat)
+    let se = find k db in
+      if matches_modes args se.sentry_mode then
+        let st = if db.use_dn then Some db.hintdb_state else None in
+        let pat = lookup_tacs concl st se in
+        merge_entry db [] pat
+      else merge_entry db [] []
 
   let is_exact = function
     | Give_exact _ -> true
@@ -490,16 +511,19 @@ module Hint_db = struct
 	    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 (next_hint_id db) v db
+    let db = if db.use_dn && rebuild then rebuild_db st' db else db in
+    let db, id = next_hint_id db in
+    addkv k id v db
 
   let add_list l db = List.fold_left (fun db k -> add_one k db) db l
 
   let remove_sdl p sdl = List.smartfilter p sdl 
-  let remove_he st p (sl1, sl2, dn, m as he) =
-    let sl1' = remove_sdl p sl1 and sl2' = remove_sdl p sl2 in
-      if sl1' == sl1 && sl2' == sl2 then he
-      else rebuild_dn st (sl1', sl2', dn, m)
+
+  let remove_he st p se =
+    let sl1' = remove_sdl p se.sentry_nopat in
+    let sl2' = remove_sdl p se.sentry_pat in
+    if sl1' == se.sentry_nopat && sl2' == se.sentry_pat then se
+    else rebuild_dn st { se with sentry_nopat = sl1'; sentry_pat = sl2' }
 
   let remove_list grs db =
     let filter (_, h) =
@@ -510,13 +534,16 @@ module Hint_db = struct
 
   let remove_one gr db = remove_list [gr] db
 
+  let get_entry se = List.map realize_tac (se.sentry_nopat @ se.sentry_pat)
+
   let iter f db =
+    let iter_se k se = f (Some k) se.sentry_mode (get_entry se) in
     f None [] (List.map (fun x -> realize_tac (snd x)) db.hintdb_nopat);
-    Constr_map.iter (fun k (l,l',_,m) -> f (Some k) m (List.map realize_tac (l@l'))) db.hintdb_map
+    Constr_map.iter iter_se db.hintdb_map
 
   let fold f db accu =
     let accu = f None [] (List.map (fun x -> snd (snd x)) db.hintdb_nopat) accu in
-    Constr_map.fold (fun k (l,l',_,m) -> f (Some k) m (List.map snd (l@l'))) db.hintdb_map accu
+    Constr_map.fold (fun k se -> f (Some k) se.sentry_mode (get_entry se)) db.hintdb_map accu
 
   let transparent_state db = db.hintdb_state
 
@@ -528,8 +555,9 @@ module Hint_db = struct
     { db with hintdb_cut = normalize_path (PathOr (db.hintdb_cut, path)) }
 
   let add_mode gr m db =
-    let (l,l',dn,ms) = find gr db in
-      { db with hintdb_map = Constr_map.add gr (l,l',dn,m :: ms) db.hintdb_map }
+    let se = find gr db in
+    let se = { se with sentry_mode = m :: se.sentry_mode } in
+    { db with hintdb_map = Constr_map.add gr se db.hintdb_map }
 
   let cut db = db.hintdb_cut
 
@@ -609,7 +637,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-	let pat = snd (Patternops.pattern_of_constr env sigma cty) in
+	let pat = pi3 (Patternops.pattern_of_constr env sigma cty) in
 	let hd =
 	  try head_pattern_bound pat
 	  with BoundPattern -> failwith "make_exact_entry"
@@ -628,7 +656,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
         let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
         let ce = mk_clenv_from_env env sigma' None (c,cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
-	let pat = snd (Patternops.pattern_of_constr env ce.evd c') in
+	let pat = pi3 (Patternops.pattern_of_constr env ce.evd c') in
         let hd =
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in
@@ -726,7 +754,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
 	      poly = poly;
-              pat = Some (snd (Patternops.pattern_of_constr env ce.evd (clenv_type ce)));
+              pat = Some (pi3 (Patternops.pattern_of_constr env ce.evd (clenv_type ce)));
 	      name = name;
               code=Res_pf_THEN_trivial_fail(c,t,ctx) })
 
@@ -782,10 +810,15 @@ let add_mode dbname l m =
   let db' = Hint_db.add_mode l m db in
     searchtable_add (dbname, db')
 
-type hint_obj = bool * string * hint_action  (* locality, name, action *)
+type hint_obj = {
+  hint_local : bool;
+  hint_name : string;
+  hint_action : hint_action;
+}
 
-let cache_autohint (_,(local,name,hints)) =
-  match hints with
+let cache_autohint (_, h) =
+  let name = h.hint_name in
+  match h.hint_action with
   | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
   | AddTransparency (grs, b) -> add_transparency name grs b
   | AddHints hints -> add_hint name hints
@@ -793,7 +826,7 @@ let cache_autohint (_,(local,name,hints)) =
   | AddCut path -> add_cut name path
   | AddMode (l, m) -> add_mode name l m
 
-let subst_autohint (subst,(local,name,hintlist as obj)) =
+let subst_autohint (subst, obj) =
   let subst_key gr =
     let (lab'', elab') = subst_global subst gr in
     let gr' =
@@ -835,29 +868,30 @@ let subst_autohint (subst,(local,name,hintlist as obj)) =
     in
     if k' == k && data' == data then hint else (k',data')
   in
-    match hintlist with
-    | CreateDB _ -> obj
+  let action = match obj.hint_action with
+    | CreateDB _ -> obj.hint_action
     | AddTransparency (grs, b) ->
-	let grs' = List.smartmap (subst_evaluable_reference subst) grs in
-	  if grs==grs' then obj else (local, name, AddTransparency (grs', b))
+      let grs' = List.smartmap (subst_evaluable_reference subst) grs in
+      if grs == grs' then obj.hint_action else AddTransparency (grs', b)
     | AddHints hintlist ->
-	let hintlist' = List.smartmap subst_hint hintlist in
-	  if hintlist' == hintlist then obj else
-	    (local,name,AddHints hintlist')
+      let hintlist' = List.smartmap subst_hint hintlist in
+      if hintlist' == hintlist then obj.hint_action else AddHints hintlist'
     | RemoveHints grs ->
-	let grs' = List.smartmap (subst_global_reference subst) grs in
-	  if grs==grs' then obj else (local, name, RemoveHints grs')
+      let grs' = List.smartmap (subst_global_reference subst) grs in
+      if grs == grs' then obj.hint_action else RemoveHints grs'
     | AddCut path ->
       let path' = subst_hints_path subst path in
-	if path' == path then obj else (local, name, AddCut path')
+      if path' == path then obj.hint_action else AddCut path'
     | AddMode (l,m) ->
       let l' = subst_global_reference subst l in
-	(local, name, AddMode (l', m))
+      if l' == l then obj.hint_action else AddMode (l', m)
+  in
+  if action == obj.hint_action then obj else { obj with hint_action = action }
 
-let classify_autohint ((local,name,hintlist) as obj) =
-  match hintlist with
+let classify_autohint obj =
+  match obj.hint_action with
   | AddHints [] -> Dispose
-  | _ -> if local then Dispose else Substitute obj
+  | _ -> if obj.hint_local then Dispose else Substitute obj
 
 let inAutoHint : hint_obj -> obj =
   declare_object {(default_object "AUTOHINT") with
@@ -866,14 +900,22 @@ let inAutoHint : hint_obj -> obj =
 		    subst_function = subst_autohint;
 		    classify_function = classify_autohint; }
 
+let make_hint ?(local = false) name action = {
+  hint_local = local;
+  hint_name = name;
+  hint_action = action;
+}
+
 let create_hint_db l n st b =
-  Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB (b, st)))
+  let hint = make_hint ~local:l n (CreateDB (b, st)) in
+  Lib.add_anonymous_leaf (inAutoHint hint)
 
 let remove_hints local dbnames grs =
   let dbnames = if List.is_empty dbnames then ["core"] else dbnames in
     List.iter
       (fun dbname ->
-	 Lib.add_anonymous_leaf (inAutoHint(local, dbname, RemoveHints grs)))
+        let hint = make_hint ~local dbname (RemoveHints grs) in
+        Lib.add_anonymous_leaf (inAutoHint hint))
       dbnames
 
 (**************************************************************************)
@@ -882,37 +924,42 @@ let remove_hints local dbnames grs =
 let add_resolves env sigma clist local dbnames =
   List.iter
     (fun dbname ->
-       Lib.add_anonymous_leaf
-	 (inAutoHint
-	    (local,dbname, AddHints
-     	      (List.flatten (List.map (fun (pri, poly, hnf, path, gr) ->
-	        make_resolves env sigma (true,hnf,Flags.is_verbose()) 
-		  pri poly ~name:path gr) clist)))))
+      let r =
+        List.flatten (List.map (fun (pri, poly, hnf, path, gr) ->
+          make_resolves env sigma (true,hnf,Flags.is_verbose()) 
+            pri poly ~name:path gr) clist)
+      in
+      let hint = make_hint ~local dbname (AddHints r) in
+      Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
 let add_unfolds l local dbnames =
   List.iter
-    (fun dbname -> Lib.add_anonymous_leaf
-       (inAutoHint (local,dbname, AddHints (List.map make_unfold l))))
+    (fun dbname ->
+      let hint = make_hint ~local dbname (AddHints (List.map make_unfold l)) in
+      Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
 let add_cuts l local dbnames =
   List.iter
-    (fun dbname -> Lib.add_anonymous_leaf
-       (inAutoHint (local,dbname, AddCut l)))
+    (fun dbname ->
+      let hint = make_hint ~local dbname (AddCut l) in
+      Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
 let add_mode l m local dbnames =
   List.iter
-    (fun dbname -> Lib.add_anonymous_leaf
-      (let m' = make_mode l m in
-	 (inAutoHint (local,dbname, AddMode (l,m')))))
+    (fun dbname ->
+      let m' = make_mode l m in
+      let hint = make_hint ~local dbname (AddMode (l, m')) in
+      Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
 let add_transparency l b local dbnames =
   List.iter
-    (fun dbname -> Lib.add_anonymous_leaf
-       (inAutoHint (local,dbname, AddTransparency (l, b))))
+    (fun dbname ->
+      let hint = make_hint ~local dbname (AddTransparency (l, b)) in
+      Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
 let add_extern pri pat tacast local dbname =
@@ -920,7 +967,7 @@ let add_extern pri pat tacast local dbname =
   | None -> None
   | Some (_, pat) -> Some pat
   in
-  let hint = local, dbname, AddHints [make_extern pri pat tacast] in
+  let hint = make_hint ~local dbname (AddHints [make_extern pri pat tacast]) in
   Lib.add_anonymous_leaf (inAutoHint hint)
 
 let add_externs pri pat tacast local dbnames =
@@ -929,9 +976,9 @@ let add_externs pri pat tacast local dbnames =
 let add_trivials env sigma l local dbnames =
   List.iter
     (fun dbname ->
-       Lib.add_anonymous_leaf (
-	 inAutoHint(local,dbname, 
-		    AddHints (List.map (fun (name, poly, c) -> make_trivial env sigma poly ~name c) l))))
+      let l = List.map (fun (name, poly, c) -> make_trivial env sigma poly ~name c) l in
+      let hint = make_hint ~local dbname (AddHints l) in
+      Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
 let (forward_intern_tac, extern_intern_tac) = Hook.make ()
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 45cf562c..958cca1c 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -28,7 +28,7 @@ val decompose_app_bound : constr -> global_reference * constr array
 
 (** Pre-created hint databases *)
 
-type 'a auto_tactic =
+type 'a auto_tactic_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
   | Give_exact of 'a
@@ -36,26 +36,27 @@ type 'a auto_tactic =
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
   | Extern     of Tacexpr.glob_tactic_expr       (* Hint Extern *)
 
+type 'a auto_tactic
+
 type hints_path_atom = 
   | PathHints of global_reference list
   | PathAny
 
-type 'a gen_auto_tactic = {
+type 'a gen_auto_tactic = private {
   pri   : int;            (** A number between 0 and 4, 4 = lower priority *)
   poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
   pat   : constr_pattern option; (** A pattern for the concl of the Goal *)
   name  : hints_path_atom; (** A potential name to refer to the hint *) 
-  code  : 'a auto_tactic; (** the tactic to apply when the concl matches pat *)
+  code  : 'a; (** the tactic to apply when the concl matches pat *)
 }
 
-type pri_auto_tactic = (constr * clausenv) gen_auto_tactic
+type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic
 
 type search_entry
 
 (** The head may not be bound. *)
 
-type hint_entry = global_reference option * 
-  (constr * types * Univ.universe_context_set) gen_auto_tactic
+type hint_entry
 
 type hints_path =
   | PathAtom of hints_path_atom
@@ -196,6 +197,13 @@ val make_extern :
   int -> constr_pattern option -> Tacexpr.glob_tactic_expr
       -> hint_entry
 
+val run_auto_tactic : 'a auto_tactic ->
+  ('a auto_tactic_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
+
+(** This function is for backward compatibility only, not to use in newly
+    written code. *)
+val repr_auto_tactic : 'a auto_tactic -> 'a auto_tactic_ast
+
 val extern_intern_tac :
   (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t
 
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index c200871e..27d25056 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Evd
 open Coqlib
 
 (** High-order patterns *)
@@ -145,8 +144,6 @@ val is_matching_sigma : constr -> bool
 val match_eqdec : constr -> bool * constr * constr * constr * constr
 
 (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
-open Proof_type
-open Tacmach
 val dest_nf_eq : [ `NF ] Proofview.Goal.t -> constr -> (constr * constr * constr)
 
 (** Match a negation *)
diff --git a/tactics/inv.mli b/tactics/inv.mli
index b3478dda..412f30c2 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Names
 open Term
 open Misctypes
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index f00ecf8f..9a64b03f 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -210,6 +210,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   end in
   let avoid = ref [] in
   let { sigma=sigma } = Proof.V82.subgoals pf in
+  let sigma = Evd.nf_constraints sigma in
   let rec fill_holes c =
     match kind_of_term c with
     | Evar (e,args) ->
@@ -222,13 +223,13 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   in
   let c = fill_holes pfterm in
   (* warning: side-effect on ownSign *)
-  let invProof = it_mkNamedLambda_or_LetIn c !ownSign
-  in
-  invProof
+  let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
+  let p = Evarutil.nf_evars_universes sigma invProof in
+    p, Evd.universe_context sigma
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
-  let invProof = inversion_scheme env sigma t sort dep inv_op in
-  let entry = definition_entry ~poly:true (*FIXME*) invProof in
+  let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in
+  let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) ~univs:ctx invProof in
   let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
   ()
 
@@ -236,7 +237,8 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
  * inv_op = InvNoThining (derives de semi inversion lemma) *)
 
 let add_inversion_lemma_exn na com comsort bool tac =
-  let env = Global.env () and evd = ref Evd.empty in
+  let env = Global.env () in
+  let evd = ref (Evd.from_env env) in
   let c = Constrintern.interp_type_evars env evd com in
   let sigma, sort = Pretyping.interp_sort !evd comsort in
   try
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 47a4de44..2f80d26f 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Names
 open Term
 open Constrexpr
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index a3914da1..ac8b4923 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -283,7 +283,7 @@ end) = struct
 	(app_poly env evd arrow [| a; b |]), unfold_impl
 	(* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *)
       else if bp then (* Dummy forall *)
-	(app_poly env evd coq_all [| a; mkLambda (Anonymous, a, b) |]), unfold_forall
+	(app_poly env evd coq_all [| a; mkLambda (Anonymous, a, lift 1 b) |]), unfold_forall
       else (* None in Prop, use arrow *)
 	(app_poly env evd arrow [| a; b |]), unfold_impl
 
@@ -629,11 +629,9 @@ let solve_remaining_by env sigma holes by =
       | None -> sigma
         (** Evar should not be defined, but just in case *)
       | Some evi ->
-        let ctx = Evd.evar_universe_context sigma in
         let env = Environ.reset_with_named_context evi.evar_hyps env in
         let ty = evi.evar_concl in
-        let c, _, ctx = Pfedit.build_by_tactic env ctx ty solve_tac in
-        let sigma = Evd.set_universe_context sigma ctx in
+        let c, sigma = Pfedit.refine_by_tactic env sigma ty solve_tac in
         Evd.define evk c sigma
     in
     List.fold_left solve sigma indep
@@ -1446,7 +1444,14 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
       let newt = Evarutil.nf_evar evars' res.rew_to in
       let evars = (* Keep only original evars (potentially instantiated) and goal evars,
 		     the rest has been defined and substituted already. *)
-	Evar.Set.fold (fun ev acc -> Evd.remove acc ev) cstrs evars'
+	Evar.Set.fold 
+	  (fun ev acc -> 
+	   if not (Evd.is_defined acc ev) then 
+	     errorlabstrm "rewrite"
+			  (str "Unsolved constraint remaining: " ++ spc () ++
+			   Evd.pr_evar_info (Evd.find acc ev))
+	   else Evd.remove acc ev) 
+	  cstrs evars'
       in
       let res = match res.rew_prf with
 	| RewCast c -> None
@@ -1466,28 +1471,32 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
           in Some proof
       in Some (Some (evars, res, newt))
 
+(** Insert a declaration after the last declaration it depends on *)
+let rec insert_dependent env decl accu hyps = match hyps with
+| [] -> List.rev_append accu [decl]
+| (id, _, _  as ndecl) :: rem ->
+  if occur_var_in_decl env id decl then
+    List.rev_append accu (decl :: hyps)
+  else
+    insert_dependent env decl (ndecl :: accu) rem
+
 let assert_replacing id newt tac = 
   let prf = Proofview.Goal.nf_enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
-    let nc' =
-      Environ.fold_named_context
-        (fun _ (n, b, t as decl) nc' ->
-          if Id.equal n id then (n, b, newt) :: nc'
-          else decl :: nc')
-        env ~init:[]
+    let ctx = Environ.named_context env in
+    let after, before = List.split_when (fun (n, b, t) -> Id.equal n id) ctx in
+    let nc = match before with
+    | [] -> assert false
+    | (id, b, _) :: rem -> insert_dependent env (id, b, newt) [] after @ rem
     in
+    let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
     Proofview.Refine.refine ~unsafe:false begin fun sigma ->
-      let env' = Environ.reset_with_named_context (val_of_named_context nc') env in
       let sigma, ev = Evarutil.new_evar env' sigma concl in
       let sigma, ev' = Evarutil.new_evar env sigma newt in
-      let fold _ (n, b, t) inst =
-        if Id.equal n id then ev' :: inst
-        else mkVar n :: inst
-      in
-      let inst = fold_named_context fold env ~init:[] in
-      let (e, args) = destEvar ev in
-      sigma, mkEvar (e, Array.of_list inst)
+      let map (n, _, _) = if Id.equal n id then ev' else mkVar n in
+      let (e, _) = destEvar ev in
+      sigma, mkEvar (e, Array.map_of_list map nc)
     end
   end in
   Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 215713d9..ab71f5f2 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -176,6 +176,13 @@ let coerce_to_evaluable_ref env v =
     let id = out_gen (topwit wit_var) v in
     if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
     else fail ()
+  else if has_type v (topwit wit_ref) then
+    let open Globnames in
+    let r = out_gen (topwit wit_ref) v in
+    match r with
+    | VarRef var -> EvalVarRef var
+    | ConstRef c -> EvalConstRef c
+    | IndRef _ | ConstructRef _ -> fail ()
   else
     let ev = match Value.to_constr v with
     | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c))
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index cb20fc93..84c0a99b 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -71,7 +71,6 @@ let interp_ml_tactic s =
 (* Summary and Object declaration *)
 
 open Nametab
-open Libnames
 open Libobject
 
 let mactab =
@@ -84,7 +83,6 @@ let is_ltac_for_ml_tactic r = fst (KNmap.find r !mactab)
 
 (* Declaration of the TAC-DEFINITION object *)
 let add (kn,td) = mactab := KNmap.add kn td !mactab
-let replace (kn,td) = mactab := KNmap.add kn td !mactab
 
 let load_md i ((sp, kn), (local, id, b, t)) = match id with
 | None ->
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index c8b9a208..5cc4c835 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -48,12 +48,10 @@ let error_tactic_expected loc =
 type glob_sign = Genintern.glob_sign = {
   ltacvars : Id.Set.t;
      (* ltac variables and the subset of vars introduced by Intro/Let/... *)
-  ltacrecvars : ltac_constant Id.Map.t;
-     (* ltac recursive names *)
   genv : Environ.env }
 
 let fully_empty_glob_sign =
-  { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = Environ.empty_env }
+  { ltacvars = Id.Set.empty; genv = Environ.empty_env }
 
 let make_empty_glob_sign () =
   { fully_empty_glob_sign with genv = Global.env () }
@@ -64,8 +62,6 @@ let find_ident id ist =
   Id.Set.mem id ist.ltacvars ||
   Id.List.mem id (ids_of_named_context (Environ.named_context ist.genv))
 
-let find_recvar qid ist = Id.Map.find qid ist.ltacrecvars
-
 (* a "var" is a ltac var or a var introduced by an intro tactic *)
 let find_var id ist = Id.Set.mem id ist.ltacvars
 
@@ -116,9 +112,7 @@ let intern_ltac_variable ist = function
       if find_var id ist then
 	(* A local variable of any type *)
 	ArgVar (loc,id)
-      else
-      (* A recursive variable *)
-      ArgArg (loc,find_recvar id ist)
+      else raise Not_found
   | _ ->
       raise Not_found
 
@@ -801,7 +795,7 @@ let glob_tactic_env l env x =
     List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
   Flags.with_option strict_check
   (intern_pure_tactic
-    { ltacvars; ltacrecvars = Id.Map.empty; genv = env })
+    { ltacvars; genv = env })
     x
 
 let split_ltac_fun = function
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index 2e662e58..a6e28d56 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -19,7 +19,6 @@ open Nametab
 
 type glob_sign = Genintern.glob_sign = {
   ltacvars : Id.Set.t;
-  ltacrecvars : ltac_constant Id.Map.t;
   genv : Environ.env }
 
 val fully_empty_glob_sign : glob_sign
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 23de47d5..f29680e1 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -318,18 +318,16 @@ let interp_ltac_var coerce ist env locid =
   try try_interp_ltac_var coerce ist env locid
   with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time")
 
-let interp_ident_gen fresh ist env sigma id =
-  try try_interp_ltac_var (coerce_to_ident fresh env) ist (Some (env,sigma)) (dloc,id)
+let interp_ident ist env sigma id =
+  try try_interp_ltac_var (coerce_to_ident false env) ist (Some (env,sigma)) (dloc,id)
   with Not_found -> id
 
-let interp_ident = interp_ident_gen false
-let interp_fresh_ident = interp_ident_gen true
-let pf_interp_ident id gl = interp_ident_gen false id (pf_env gl) (project gl)
+let pf_interp_ident id gl = interp_ident id (pf_env gl) (project gl)
 
-(* Interprets an optional identifier which must be fresh *)
-let interp_fresh_name ist env sigma = function
+(* Interprets an optional identifier, bound or fresh *)
+let interp_name ist env sigma = function
   | Anonymous -> Anonymous
-  | Name id -> Name (interp_fresh_ident ist env sigma id)
+  | Name id -> Name (interp_ident ist env sigma id)
 
 let interp_intro_pattern_var loc ist env sigma id =
   try try_interp_ltac_var (coerce_to_intro_pattern env) ist (Some (env,sigma)) (loc,id)
@@ -497,8 +495,6 @@ let interp_fresh_id ist env sigma l =
       Id.of_string s in
   Tactics.fresh_id_in_env avoid id env
 
-
-
 (* Extract the uconstr list from lfun *)
 let extract_ltac_constr_context ist env =
   let open Glob_term in
@@ -683,7 +679,7 @@ let interp_constr_with_occurrences ist env sigma (occs,c) =
 let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
   let p = match a with
   | Inl b -> Inl (interp_evaluable ist env sigma b)
-  | Inr c -> Inr (snd (interp_typed_pattern ist env sigma c)) in
+  | Inr c -> Inr (pi3 (interp_typed_pattern ist env sigma c)) in
   interp_occurrences ist occs, p
 
 let interp_constr_with_occurrences_and_name_as_list =
@@ -694,7 +690,7 @@ let interp_constr_with_occurrences_and_name_as_list =
     (fun ist env sigma (occ_c,na) ->
       let (sigma,c_interp) = interp_constr_with_occurrences ist env sigma occ_c in
       sigma, (c_interp,
-       interp_fresh_name ist env sigma na))
+       interp_name ist env sigma na))
 
 let interp_red_expr ist env sigma = function
   | Unfold l -> sigma , Unfold (List.map (interp_unfold ist env sigma) l)
@@ -844,7 +840,7 @@ let rec interp_intro_pattern ist env sigma = function
   | loc, IntroForthcoming _  as x -> sigma, x
 
 and interp_intro_pattern_naming loc ist env sigma = function
-  | IntroFresh id -> IntroFresh (interp_fresh_ident ist env sigma id)
+  | IntroFresh id -> IntroFresh (interp_ident ist env sigma id)
   | IntroIdentifier id -> interp_intro_pattern_naming_var loc ist env sigma id
   | IntroAnonymous as x -> x
 
@@ -1032,7 +1028,7 @@ let use_types = false
 
 let eval_pattern lfun ist env sigma (_,pat as c) =
   if use_types then
-    snd (interp_typed_pattern ist env sigma c)
+    pi3 (interp_typed_pattern ist env sigma c)
   else
     instantiate_pattern env sigma lfun pat
 
@@ -1189,7 +1185,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       msg_warning
 	(strbrk "The general \"info\" tactic is currently not working." ++ spc()++
            strbrk "There is an \"Info\" command to replace it." ++fnl () ++
-	   strbrk "Some specific verbose tactics may also exist, such as info_trivial, info_auto, info_eauto.");
+	   strbrk "Some specific verbose tactics may also exist, such as info_eauto.");
       eval_tactic ist tac
   (* For extensions *)
   | TacAlias (loc,s,l) ->
@@ -1215,7 +1211,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
           | IntOrVarArgType ->
               Ftactic.return (mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x))
           | IdentArgType ->
-              Ftactic.return (value_of_ident (interp_fresh_ident ist env sigma
+              Ftactic.return (value_of_ident (interp_ident ist env sigma
                                                (out_gen (glbwit wit_ident) x)))
           | VarArgType ->
               Ftactic.return (mk_hyp_value ist env sigma (out_gen (glbwit wit_var) x))
@@ -1256,7 +1252,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
               Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans)
           | ListArgType IdentArgType ->
               let wit = glbwit (wit_list wit_ident) in
-              let mk_ident x = value_of_ident (interp_fresh_ident ist env sigma x) in
+              let mk_ident x = value_of_ident (interp_ident ist env sigma x) in
               let ans = List.map mk_ident (out_gen wit x) in
               Ftactic.return (in_gen (topwit (wit_list wit_genarg)) ans)
           | ListArgType t  ->
@@ -1624,7 +1620,7 @@ and interp_genarg ist env sigma concl gl x =
         (ArgArg (interp_int_or_var ist (out_gen (glbwit wit_int_or_var) x)))
     | IdentArgType ->
       in_gen (topwit wit_ident)
-        (interp_fresh_ident ist env sigma (out_gen (glbwit wit_ident) x))
+        (interp_ident ist env sigma (out_gen (glbwit wit_ident) x))
     | VarArgType ->
       in_gen (topwit wit_var) (interp_hyp ist env sigma (out_gen (glbwit wit_var) x))
     | GenArgType ->
@@ -1785,19 +1781,19 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in
-        Proofview.Unsafe.tclEVARS sigma <*>
-        name_atomic ~env
+        Tacticals.New.tclWITHHOLES false 
+        (name_atomic ~env
           (TacIntroPattern l)
           (* spiwack: print uninterpreted, not sure if it is the
              expected behaviour. *)
-          (Tactics.intros_patterns l')
+          (Tactics.intros_patterns l')) sigma
       end
   | TacIntroMove (ido,hto) ->
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let mloc = interp_move_location ist env sigma hto in
-        let ido = Option.map (interp_fresh_ident ist env sigma) ido in
+        let ido = Option.map (interp_ident ist env sigma) ido in
         name_atomic ~env
           (TacIntroMove(ido,mloc))
           (Tactics.intro_move ido mloc)
@@ -1824,11 +1820,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
 	    (k,(loc,f))) cb 
 	in
         let sigma,tac = match cl with
-          | None -> sigma, fun l -> Tactics.apply_with_delayed_bindings_gen a ev l
+          | None -> sigma, Tactics.apply_with_delayed_bindings_gen a ev l
           | Some cl ->
               let sigma,(clear,id,cl) = interp_in_hyp_as ist env sigma cl in
-              sigma, fun l -> Tactics.apply_delayed_in a ev clear id l cl in
-        Tacticals.New.tclWITHHOLES ev tac sigma l
+              sigma, Tactics.apply_delayed_in a ev clear id l cl in
+        Tacticals.New.tclWITHHOLES ev tac sigma
       end
       end
   | TacElim (ev,(keep,cb),cbo) ->
@@ -1837,28 +1833,28 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let sigma = Proofview.Goal.sigma gl in 
         let sigma, cb = interp_constr_with_bindings ist env sigma cb in
         let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
-        let named_tac cbo =
+        let named_tac =
           let tac = Tactics.elim ev keep cb cbo in
           name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac
         in
-        Tacticals.New.tclWITHHOLES ev named_tac sigma cbo
+        Tacticals.New.tclWITHHOLES ev named_tac sigma
       end
   | TacCase (ev,(keep,cb)) ->
       Proofview.Goal.enter begin fun gl ->
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
         let sigma, cb = interp_constr_with_bindings ist env sigma cb in
-        let named_tac cb =
+        let named_tac =
           let tac = Tactics.general_case_analysis ev keep cb in
           name_atomic ~env (TacCase(ev,(keep,cb))) tac
         in
-        Tacticals.New.tclWITHHOLES ev named_tac sigma cb
+        Tacticals.New.tclWITHHOLES ev named_tac sigma
       end
   | TacFix (idopt,n) ->
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
-        let idopt = Option.map (interp_fresh_ident ist env sigma) idopt in
+        let idopt = Option.map (interp_ident ist env sigma) idopt in
         name_atomic ~env
           (TacFix(idopt,n))
           (Proofview.V82.tactic (Tactics.fix idopt n))
@@ -1870,13 +1866,13 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = pf_env gl in
         let f sigma (id,n,c) =
 	  let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
-	  sigma , (interp_fresh_ident ist env sigma id,n,c_interp) in
+	  sigma , (interp_ident ist env sigma id,n,c_interp) in
         let (sigma,l_interp) =
           Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
         in
         tclTHEN
 	  (tclEVARS sigma)
-	  (Tactics.mutual_fix (interp_fresh_ident ist env sigma id) n l_interp 0)
+	  (Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0)
           gl
       end
       end
@@ -1884,7 +1880,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
-        let idopt = Option.map (interp_fresh_ident ist env sigma) idopt in
+        let idopt = Option.map (interp_ident ist env sigma) idopt in
         name_atomic ~env
           (TacCofix (idopt))
           (Proofview.V82.tactic (Tactics.cofix idopt))
@@ -1896,13 +1892,13 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = pf_env gl in
         let f sigma (id,c) =
 	  let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
-	  sigma , (interp_fresh_ident ist env sigma id,c_interp) in
+	  sigma , (interp_ident ist env sigma id,c_interp) in
         let (sigma,l_interp) =
           Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
         in
         tclTHEN
 	  (tclEVARS sigma)
-	  (Tactics.mutual_cofix (interp_fresh_ident ist env sigma id) l_interp 0)
+	  (Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0)
           gl
       end
       end
@@ -1915,20 +1911,20 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in
         let tac = Option.map (interp_tactic ist) t in
-        Proofview.Unsafe.tclEVARS sigma <*>
-        name_atomic ~env
+        Tacticals.New.tclWITHHOLES false
+        (name_atomic ~env
           (TacAssert(b,t,ipat,c))
-          (Tactics.forward b tac ipat' c)
+          (Tactics.forward b tac ipat' c)) sigma
       end
   | TacGeneralize cl ->
       Proofview.Goal.enter begin fun gl ->
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
         let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
-        Proofview.Unsafe.tclEVARS sigma <*>
-        name_atomic ~env
+        Tacticals.New.tclWITHHOLES false
+        (name_atomic ~env
           (TacGeneralize cl)
-          (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl))
+          (Proofview.V82.tactic (Tactics.Simple.generalize_gen cl))) sigma
       end
   | TacGeneralizeDep c ->
       (new_interp_constr ist c) (fun c ->
@@ -1953,11 +1949,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
             let with_eq = if b then None else Some (true,id) in
             Tactics.letin_tac with_eq na c None cl
           in
-	  Proofview.Unsafe.tclEVARS sigma <*>
-          let na = interp_fresh_name ist env sigma na in
-          name_atomic ~env
+          let na = interp_name ist env sigma na in
+          Tacticals.New.tclWITHHOLES false
+          (name_atomic ~env
             (TacLetTac(na,c_interp,clp,b,eqpat))
-            (let_tac b na c_interp clp eqpat)
+            (let_tac b na c_interp clp eqpat)) sigma
         else
         (* We try to keep the pattern structure as much as possible *)
           let let_pat_tac b na c cl eqpat =
@@ -1969,12 +1965,18 @@ and interp_atomic ist tac : unit Proofview.tactic =
           name_atomic ~env
             (TacLetTac(na,c,clp,b,eqpat))
 	    (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*)
-               (let_pat_tac b (interp_fresh_name ist env sigma na)
-                  ((sigma,sigma'),c) clp) sigma' eqpat)
+               (let_pat_tac b (interp_name ist env sigma na)
+                  ((sigma,sigma'),c) clp eqpat) sigma')
       end
 
   (* Automation tactics *)
   | TacTrivial (debug,lems,l) ->
+      begin if debug == Tacexpr.Info then
+          msg_warning
+	    (strbrk"The \"info_trivial\" tactic" ++ spc ()
+           ++strbrk"does not print traces anymore." ++ spc()
+           ++strbrk"Use \"Info 1 trivial\", instead.")
+      end;
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
@@ -1986,6 +1988,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
 	     (Option.map (List.map (interp_hint_base ist)) l))
       end
   | TacAuto (debug,n,lems,l) ->
+      begin if debug == Tacexpr.Info then
+          msg_warning
+	    (strbrk"The \"info_auto\" tactic" ++ spc ()
+           ++strbrk"does not print traces anymore." ++ spc()
+           ++strbrk"Use \"Info 1 auto\", instead.")
+      end;
       Proofview.Goal.enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
@@ -2067,7 +2075,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let l =
           List.map (fun (id1,id2) ->
 	    interp_hyp ist env sigma id1,
-	    interp_fresh_ident ist env sigma (snd id2)) l
+	    interp_ident ist env sigma (snd id2)) l
         in
         name_atomic ~env
           (TacRename l)
@@ -2080,11 +2088,11 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
-        let named_tac bll =
+        let named_tac =
           let tac = Tactics.split_with_bindings ev bll in
           name_atomic ~env (TacSplit (ev, bll)) tac
         in
-        Tacticals.New.tclWITHHOLES ev named_tac sigma bll
+        Tacticals.New.tclWITHHOLES ev named_tac sigma
       end
   (* Conversion *)
   | TacReduce (r,cl) ->
@@ -2111,7 +2119,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
           | AllOccurrences | NoOccurrences -> true
           | _ -> false
         in
-        let c_interp sigma =
+        let c_interp patvars sigma =
+	  let lfun' = Id.Map.fold (fun id c lfun ->
+	    Id.Map.add id (Value.of_constr c) lfun) 
+	    patvars ist.lfun
+	  in
+	  let ist = { ist with lfun = lfun' } in
 	  if is_onhyps && is_onconcl
 	  then interp_type ist (pf_env gl) sigma c
 	  else interp_constr ist (pf_env gl) sigma c
@@ -2128,16 +2141,20 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = Proofview.Goal.sigma gl in
         Proofview.V82.tactic begin fun gl -> 
-          let sign,op = interp_typed_pattern ist env sigma op in
+          let (sigma,sign,op) = interp_typed_pattern ist env sigma op in
           let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
-	  let env' = Environ.push_named_context sign env in
-          let c_interp sigma =
-	      try interp_constr ist env' sigma c
+          let c_interp patvars sigma =
+	    let lfun' = Id.Map.fold (fun id c lfun ->
+	      Id.Map.add id (Value.of_constr c) lfun) 
+	      patvars ist.lfun
+	    in
+	    let ist = { ist with lfun = lfun' } in
+	      try interp_constr ist env sigma c
 	      with e when to_catch e (* Hack *) ->
 		errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
           in
-	      (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl))
-		gl
+	    (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl))
+	      { gl with sigma = sigma }
         end
       end
       end
@@ -2184,10 +2201,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
         in
         let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in
         let sigma,ids_interp = interp_or_and_intro_pattern_option ist env sigma ids in
-        Proofview.Unsafe.tclEVARS sigma <*>
-        name_atomic ~env
+        Tacticals.New.tclWITHHOLES false
+        (name_atomic ~env
           (TacInversion(DepInversion(k,c_interp,ids),dqhyps))
-          (Inv.dinv k c_interp ids_interp dqhyps)
+          (Inv.dinv k c_interp ids_interp dqhyps)) sigma
       end
   | TacInversion (NonDepInversion (k,idl,ids),hyp) ->
       Proofview.Goal.enter begin fun gl ->
@@ -2196,10 +2213,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let hyps = interp_hyp_list ist env sigma idl in
         let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in
         let sigma, ids_interp = interp_or_and_intro_pattern_option ist env sigma ids in
-        Proofview.Unsafe.tclEVARS sigma <*>
-        name_atomic ~env
+        Tacticals.New.tclWITHHOLES false
+        (name_atomic ~env
           (TacInversion (NonDepInversion (k,hyps,ids),dqhyps))
-          (Inv.inv_clause k ids_interp hyps dqhyps)
+          (Inv.inv_clause k ids_interp hyps dqhyps)) sigma
       end
   | TacInversion (InversionUsing (c,idl),hyp) ->
       Proofview.Goal.enter begin fun gl ->
@@ -2241,8 +2258,7 @@ let interp_tac_gen lfun avoid_ids debug t =
   let ltacvars = Id.Map.domain lfun in
   interp_tactic ist
     (intern_pure_tactic {
-      ltacvars; ltacrecvars = Id.Map.empty;
-      genv = env } t)
+      ltacvars; genv = env } t)
   end
 
 let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
@@ -2252,8 +2268,7 @@ let _ = Proof_global.set_interp_tac interp
 (* [global] means that [t] should be internalized outside of goals. *)
 let hide_interp global t ot =
   let hide_interp env =
-    let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
-                genv = env } in
+    let ist = { ltacvars = Id.Set.empty; genv = env } in
     let te = intern_pure_tactic ist t in
     let t = eval_tactic te in
     match ot with
@@ -2349,39 +2364,7 @@ let _ =
     if has_type arg (glbwit wit_tactic) then
       let tac = out_gen (glbwit wit_tactic) arg in
       let tac = interp_tactic ist tac in
-      (** Save the initial side-effects to restore them afterwards. We set the
-          current set of side-effects to be empty so that we can retrieve the
-          ones created during the tactic invocation easily. *)
-      let eff = Evd.eval_side_effects sigma in
-      let sigma = Evd.drop_side_effects sigma in
-      (** Start a proof *)
-      let prf = Proof.start sigma [env, ty] in
-      let (prf, _) =
-        try Proof.run_tactic env tac prf
-        with Logic_monad.TacticFailure e as src ->
-          (** Catch the inner error of the monad tactic *)
-          let (_, info) = Errors.push src in
-          iraise (e, info)
-      in
-      (** Plug back the retrieved sigma *)
-      let sigma = Proof.in_proof prf (fun sigma -> sigma) in
-      let ans = match Proof.initial_goals prf with
-      | [c, _] -> c
-      | _ -> assert false
-      in
-      let ans = Reductionops.nf_evar sigma ans in
-      (** [neff] contains the freshly generated side-effects *)
-      let neff = Evd.eval_side_effects sigma in
-      (** Reset the old side-effects *)
-      let sigma = Evd.drop_side_effects sigma in
-      let sigma = Evd.emit_side_effects eff sigma in
-      (** Get rid of the fresh side-effects by internalizing them in the term
-          itself. Note that this is unsound, because the tactic may have solved
-          other goals that were already present during its invocation, so that
-          those goals rely on effects that are not present anymore. Hopefully,
-          this hack will work in most cases. *)
-      let ans = Term_typing.handle_side_effects env ans neff in
-      ans, sigma
+      Pfedit.refine_by_tactic env sigma ty tac
     else
       failwith "not a tactic"
   in
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 59cd065d..afffaffb 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -27,9 +27,8 @@ let subst_quantified_hypothesis _ x = x
 
 let subst_declared_or_quantified_hypothesis _ x = x
 
-let subst_glob_constr_and_expr subst (c,e) =
-  assert (Option.is_empty e); (* e<>None only for toplevel tactics *)
-  (Detyping.subst_glob_constr subst c,None)
+let subst_glob_constr_and_expr subst (c, e) =
+  (Detyping.subst_glob_constr subst c, e)
 
 let subst_glob_constr = subst_glob_constr_and_expr (* shortening *)
 
@@ -100,20 +99,11 @@ let subst_evaluable subst =
   let subst_eval_ref = subst_evaluable_reference subst in
     subst_or_var (subst_and_short_name subst_eval_ref)
 
-let subst_unfold subst (l,e) =
-  (l,subst_evaluable subst e)
-
-let subst_flag subst red =
-  { red with rConst = List.map (subst_evaluable subst) red.rConst }
-
 let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
 
 let subst_glob_constr_or_pattern subst (c,p) =
   (subst_glob_constr subst c,subst_pattern subst p)
 
-let subst_pattern_with_occurrences subst (l,p) =
-  (l,subst_glob_constr_or_pattern subst p)
-
 let subst_redexp subst =
   Miscops.map_red_expr_gen
     (subst_glob_constr subst)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index cf2126f8..9b16fe3f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -16,7 +16,6 @@ open Context
 open Declarations
 open Tacmach
 open Clenv
-open Misctypes
 
 (************************************************************************)
 (* Tacticals re-exported from the Refiner module                        *)
@@ -494,26 +493,23 @@ module New = struct
       let (loc,_) = evi.Evd.evar_source in
       Pretype_errors.error_unsolvable_implicit loc env sigma evk None
 
-  let tclWITHHOLES accept_unresolved_holes tac sigma x =
+  let tclWITHHOLES accept_unresolved_holes tac sigma =
     tclEVARMAP >>= fun sigma_initial ->
-      if sigma == sigma_initial then tac x
+      if sigma == sigma_initial then tac
       else
-        let check_evars env new_sigma sigma initial_sigma =
-          try
-            check_evars env new_sigma sigma initial_sigma;
-            tclUNIT ()
-          with e when Errors.noncritical e ->
-            tclZERO e
-        in
-        let check_evars_if =
+        let check_evars_if x =
           if not accept_unresolved_holes then
             tclEVARMAP >>= fun sigma_final ->
               tclENV >>= fun env ->
-                check_evars env sigma_final sigma sigma_initial
+                try
+                  let () = check_evars env sigma_final sigma sigma_initial in
+                  tclUNIT x
+                with e when Errors.noncritical e ->
+                  tclZERO e
           else
-            tclUNIT ()
+            tclUNIT x
         in
-        Proofview.Unsafe.tclEVARS sigma <*> tac x <*> check_evars_if
+        Proofview.Unsafe.tclEVARS sigma <*> tac >>= check_evars_if
 
   let tclTIMEOUT n t =
     Proofview.tclOR
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 6249bbc5..4e860892 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -6,14 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Pp
 open Names
 open Term
 open Context
 open Tacmach
 open Proof_type
-open Clenv
 open Tacexpr
 open Locus
 open Misctypes
@@ -220,7 +218,7 @@ module New : sig
   val tclCOMPLETE : 'a tactic -> 'a tactic
   val tclSOLVE : unit tactic list -> unit tactic
   val tclPROGRESS : unit tactic -> unit tactic
-  val tclWITHHOLES : bool -> ('a -> unit tactic) -> Evd.evar_map -> 'a -> unit tactic
+  val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
 
   val tclTIMEOUT : int -> unit tactic -> unit tactic
   val tclTIME : string option -> 'a tactic -> 'a tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f1f1248d..7484139c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -59,22 +59,7 @@ let dloc = Loc.ghost
 
 let typ_of = Retyping.get_type_of
 
-(* Option for 8.4 compatibility *)
 open Goptions
-let legacy_elim_if_not_fully_applied_argument = ref false
-
-let use_legacy_elim_if_not_fully_applied_argument () =
-  !legacy_elim_if_not_fully_applied_argument
-  || Flags.version_less_or_equal Flags.V8_4
-
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
-      optname  = "partially applied elimination argument legacy";
-      optkey   = ["Legacy";"Partially";"Applied";"Elimination";"Argument"];
-      optread  = (fun () -> !legacy_elim_if_not_fully_applied_argument) ;
-      optwrite = (fun b -> legacy_elim_if_not_fully_applied_argument := b) }
 
 (* Option for 8.2 compatibility *)
 let dependent_propositions_elimination = ref true
@@ -440,7 +425,7 @@ let pf_reduce_decl redfun where (id,c,ty) gl =
   match c with
   | None ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str "has no value.");
+	errorlabstrm "" (pr_id id ++ str " has no value.");
       (id,None,redfun' ty)
   | Some b ->
       let b' = if where != InHypTypeOnly then redfun' b else b in
@@ -537,7 +522,7 @@ let pf_e_reduce_decl redfun where (id,c,ty) gl =
   match c with
   | None ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str "has no value.");
+	errorlabstrm "" (pr_id id ++ str " has no value.");
     let sigma, ty' = redfun sigma ty in
       sigma, (id,None,ty')
   | Some b ->
@@ -580,12 +565,16 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env
   match c with
   | None ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str "has no value.");
+	errorlabstrm "" (pr_id id ++ str " has no value.");
     let sigma',ty' = redfun false env sigma ty in
       sigma', (id,None,ty')
   | Some b ->
-      let sigma',b' = if where != InHypTypeOnly then redfun true env sigma b else sigma, b in
-      let sigma',ty' = if where != InHypValueOnly then redfun false env sigma ty else sigma', ty in
+      let sigma',b' = 
+	if where != InHypTypeOnly then redfun true env sigma b else sigma, b 
+      in
+      let sigma',ty' = 
+	if where != InHypValueOnly then redfun false env sigma' ty else sigma', ty 
+      in
 	sigma', (id,Some b',ty')
 
 let e_change_in_hyp redfun (id,where) =
@@ -595,7 +584,10 @@ let e_change_in_hyp redfun (id,where) =
       (Proofview.Goal.env gl) (Proofview.Goal.sigma gl))
     convert_hyp
 
-type change_arg = evar_map -> evar_map * constr
+type change_arg = Pattern.patvar_map -> evar_map -> evar_map * constr
+
+let make_change_arg c =
+  fun pats sigma -> (sigma, replace_vars (Id.Map.bindings pats) c)
 
 let check_types env sigma mayneedglobalcheck deep newc origc =
   let t1 = Retyping.get_type_of env sigma newc in
@@ -623,21 +615,15 @@ let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
   if not b then errorlabstrm "convert-check-hyp" (str "Not convertible.");
   sigma, t'
 
-let change_and_check_subst cv_pb mayneedglobalcheck subst t env sigma c =
-  let t' sigma =
-    let sigma, t = t sigma in
-      sigma, replace_vars (Id.Map.bindings subst) t 
-  in change_and_check cv_pb mayneedglobalcheck true t' env sigma c
-
 (* Use cumulativity only if changing the conclusion not a subterm *)
 let change_on_subterm cv_pb deep t where env sigma c =
   let mayneedglobalcheck = ref false in
   let sigma,c = match where with
-  | None -> change_and_check cv_pb mayneedglobalcheck deep t env sigma c
+  | None -> change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c
   | Some occl ->
       e_contextually false occl
         (fun subst ->
-          change_and_check_subst Reduction.CONV mayneedglobalcheck subst t)
+          change_and_check Reduction.CONV mayneedglobalcheck true (t subst))
         env sigma c in
   if !mayneedglobalcheck then
     begin
@@ -667,7 +653,7 @@ let change chg c cls gl =
     cls) gl
 
 let change_concl t = 
-  change_in_concl None (fun sigma -> sigma, t)
+  change_in_concl None (make_change_arg t)
 
 (* Pour usage interne (le niveau User est pris en compte par reduce) *)
 let red_in_concl        = reduct_in_concl (red_product,REVERTcast)
@@ -780,8 +766,6 @@ let intro = intro_gen (NamingAvoid []) MoveLast false false
 let introf = intro_gen (NamingAvoid []) MoveLast true false
 let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false
 
-let intro_then_force = intro_then_gen (NamingAvoid []) MoveLast true false
-
 let intro_move_avoid idopt avoid hto = match idopt with
   | None -> intro_gen (NamingAvoid avoid) hto true false
   | Some id -> intro_gen (NamingMustBe (dloc,id)) hto true false
@@ -895,7 +879,7 @@ let msg_quantified_hypothesis = function
   | NamedHyp id ->
       str "quantified hypothesis named " ++ pr_id id
   | AnonHyp n ->
-      int n ++ str (match n with 1 -> "st" | 2 -> "nd" | _ -> "th") ++
+      pr_nth n ++
       str " non dependent hypothesis"
 
 let depth_of_quantified_hypothesis red h gl =
@@ -1135,11 +1119,18 @@ let enforce_prop_bound_names rename tac =
   | _ ->
       tac
 
+let rec contract_letin_in_lam_header c =
+  match kind_of_term c with
+  | Lambda (x,t,c)  -> mkLambda (x,t,contract_letin_in_lam_header c)
+  | LetIn (x,b,t,c) -> contract_letin_in_lam_header (subst1 b c)
+  | _ -> c
+
 let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ()) 
     rename i (elim, elimty, bindings) indclause =
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
+  let elim = contract_letin_in_lam_header elim in
   let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
   let indmv =
     (match kind_of_term (nth_arg i elimclause.templval.rebus) with
@@ -1293,6 +1284,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
+  let elim = contract_letin_in_lam_header elim in
   let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
   let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
   let hypmv =
@@ -1518,7 +1510,7 @@ let apply_with_delayed_bindings_gen b e l =
       let env = Proofview.Goal.env gl in
       let sigma, cb = f env sigma in
 	Tacticals.New.tclWITHHOLES e
-          (general_apply b b e k) sigma (loc,cb)
+          (general_apply b b e k (loc,cb)) sigma
     end
   in
   let rec aux = function
@@ -1621,8 +1613,8 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
     let sigma, c = f env sigma in
     Tacticals.New.tclWITHHOLES with_evars 
       (apply_in_once sidecond_first with_delta with_destruct with_evars
-         naming id (clear_flag,(loc,c)))
-      sigma tac
+         naming id (clear_flag,(loc,c)) tac)
+      sigma
   end
 
 (* A useful resolution tactic which, if c:A->B, transforms |- C into
@@ -1975,21 +1967,25 @@ let intro_decomp_eq_function = ref (fun _ -> failwith "Not implemented")
 let declare_intro_decomp_eq f = intro_decomp_eq_function := f
 
 let my_find_eq_data_decompose gl t =
-  try find_eq_data_decompose gl t
+  try Some (find_eq_data_decompose gl t)
   with e when is_anomaly e
     (* Hack in case equality is not yet defined... one day, maybe,
        known equalities will be dynamically registered *)
-      -> raise Constr_matching.PatternMatchingFailure
+      -> None
+  | Constr_matching.PatternMatchingFailure -> None
 
 let intro_decomp_eq loc l thin tac id =
   Proofview.Goal.nf_enter begin fun gl ->
   let c = mkVar id in
   let t = Tacmach.New.pf_type_of gl c in
   let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in
-  let eq,u,eq_args = my_find_eq_data_decompose gl t in
-  !intro_decomp_eq_function
+  match my_find_eq_data_decompose gl t with
+  | Some (eq,u,eq_args) ->
+    !intro_decomp_eq_function
     (fun n -> tac ((dloc,id)::thin) (Some (true,n)) l)
     (eq,t,eq_args) (c, t)
+  | None ->
+    Tacticals.New.tclZEROMSG (str "Not a primitive equality here.")
   end
 
 let intro_or_and_pattern loc bracketed ll thin tac id =
@@ -2151,12 +2147,12 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
         let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
         let sigma,c = f env sigma in
-        Proofview.Unsafe.tclEVARS sigma <*>
+        Tacticals.New.tclWITHHOLES false
           (Tacticals.New.tclTHENFIRST
              (* Skip the side conditions of the apply *)
              (apply_in_once false true true true naming id
-                (None,(sigma,(c,NoBindings))) tac_ipat))
-	  (tac thin None [])
+                (None,(sigma,(c,NoBindings))) tac_ipat) (tac thin None []))
+          sigma
       end
 
 and prepare_intros_loc loc dft = function
@@ -2327,7 +2323,10 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
       let heq = match ido with
       | IntroAnonymous -> fresh_id_in_env [id] (add_prefix "Heq" id) env
       | IntroFresh heq_base -> fresh_id_in_env [id] heq_base env
-      | IntroIdentifier id -> id in
+      | IntroIdentifier id ->
+          if List.mem id (ids_of_named_context (named_context env)) then
+            user_err_loc (loc,"",pr_id id ++ str" is already used.");
+          id in
       let eqdata = build_coq_eq_data () in
       let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
       let sigma, eq = Evd.fresh_global env sigma eqdata.eq in
@@ -2767,7 +2766,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
     if Int.equal i nparams then
       let t = applist (hd, params@args) in
       Tacticals.New.tclTHEN
-        (change_in_hyp None (fun sigma -> sigma, t) (hyp0,InHypTypeOnly))
+        (change_in_hyp None (make_change_arg t) (hyp0,InHypTypeOnly))
         (tac avoid)
     else
       let c = List.nth argl (i-1) in
@@ -2805,12 +2804,6 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
   atomize_one (List.length argl) [] []
   end
 
-let find_atomic_param_of_ind nparams indtyp =
-  let argl = snd (decompose_app indtyp) in
-  let params,args = List.chop nparams argl in
-  let test c = isVar c && not (List.exists (dependent c) params) in
-  List.map destVar (List.filter test args)
-
 (* [cook_sign] builds the lists [beforetoclear] (preceding the
    ind. var.) and [aftertoclear] (coming after the ind. var.)  of hyps
    that must be erased, the lists of hyps to be generalize [decldeps] on the
@@ -3668,6 +3661,7 @@ let induction_tac with_evars params indvars elim gl =
   let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in
   let i = match i with None -> index_of_ind_arg elimt | Some i -> i in
   (* elimclause contains this: (elimc ?i ?j ?k...?l) *)
+  let elimc = contract_letin_in_lam_header elimc in
   let elimc = mkCast (elimc, DEFAULTcast, elimt) in
   let elimclause =
     pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in
@@ -3784,7 +3778,7 @@ let clear_unselected_context id inhyps cls gl =
       thin ids gl
   | None -> tclIDTAC gl
 
-let use_bindings env sigma elim (c,lbind) typ =
+let use_bindings env sigma elim must_be_closed (c,lbind) typ =
   let typ =
     if elim == None then
       (* w/o an scheme, the term has to be applied at least until
@@ -3803,6 +3797,8 @@ let use_bindings env sigma elim (c,lbind) typ =
   let rec find_clause typ =
     try
       let indclause = make_clenv_binding env sigma (c,typ) lbind in
+      if must_be_closed && occur_meta (clenv_value indclause) then
+        error "Need a fully applied argument.";
       (* We lose the possibility of coercions in with-bindings *)
       pose_all_metas_as_evars env indclause.evd (clenv_value indclause)
     with e when catchable_exception e ->
@@ -3848,7 +3844,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
   let ccl = Proofview.Goal.raw_concl gl in
   let store = Proofview.Goal.extra gl in
   let check = check_enough_applied env sigma elim in
-  let (sigma',c) = use_bindings env sigma elim (c0,lbind) t0 in
+  let (sigma',c) = use_bindings env sigma elim false (c0,lbind) t0 in
   let abs = AbstractPattern (from_prefix,check,Name id,(pending,c),cls,false) in
   let (id,sign,_,lastlhyp,ccl,res) = make_abstraction env sigma' ccl abs in
   match res with
@@ -3868,7 +3864,8 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
       (Tacticals.New.tclTHENLIST [
         Proofview.Unsafe.tclEVARS sigma;
         Proofview.Refine.refine ~unsafe:true (fun sigma ->
-          let (sigma,c) = use_bindings env sigma elim (c0,lbind) t0 in
+          let b = not with_evars && with_eq != None in
+          let (sigma,c) = use_bindings env sigma elim b (c0,lbind) t0 in
           let t = Retyping.get_type_of env sigma c in
           mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t));
         Proofview.(if with_evars then shelve_unifiable else guard_no_unifiable);
@@ -4411,11 +4408,6 @@ let tclABSTRACT name_op tac =
   in
   abstract_subproof s gk tac
 
-let admit_as_an_axiom =
-  Proofview.tclUNIT () >>= fun () -> (* delay for Coqlib.build_coq_proof_admitted *)
-  simplest_case (Coqlib.build_coq_proof_admitted ()) <*>
-  Proofview.mark_as_unsafe
-
 let unify ?(state=full_transparent_state) x y =
   Proofview.Goal.nf_enter begin fun gl ->
   try
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6025883f..0069d100 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -125,8 +125,9 @@ val exact_proof      : Constrexpr.constr_expr -> tactic
 
 type tactic_reduction = env -> evar_map -> constr -> constr
 
-type change_arg = evar_map -> evar_map * constr
+type change_arg = patvar_map -> evar_map -> evar_map * constr
 
+val make_change_arg   : constr -> change_arg
 val reduct_in_hyp     : ?check:bool -> tactic_reduction -> hyp_location -> tactic
 val reduct_option     : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> tactic
 val reduct_in_concl   : tactic_reduction * cast_kind -> tactic
@@ -393,8 +394,6 @@ val unify           : ?state:Names.transparent_state -> constr -> constr -> unit
 
 val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
 
-val admit_as_an_axiom : unit Proofview.tactic
-
 val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic
 val specialize_eqs : Id.t -> tactic
 
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index e637b2e3..e79fc6dc 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -371,6 +371,17 @@ struct
   let find_all dn = Idset.elements (TDnet.find_all dn)
 
   let map f dn = TDnet.map f (fun x -> x) dn
+
+  let refresh_metas dn =
+    let new_metas = ref Int.Map.empty in
+    let refresh_one_meta i =
+      try Int.Map.find i !new_metas
+      with Not_found ->
+        let new_meta = fresh_meta () in
+        let () = new_metas := Int.Map.add i new_meta !new_metas in
+        new_meta
+    in
+    TDnet.map_metas refresh_one_meta dn
 end
 
 module type S =
@@ -385,4 +396,5 @@ sig
   val search_pattern : t -> constr -> ident list
   val find_all : t -> ident list
   val map : (ident -> ident) -> t -> t
+  val refresh_metas : t -> t
 end
diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli
index a5c80cc0..58f95ac6 100644
--- a/tactics/term_dnet.mli
+++ b/tactics/term_dnet.mli
@@ -80,6 +80,8 @@ sig
   val find_all : t -> ident list
 
   val map : (ident -> ident) -> t -> t
+
+  val refresh_metas : t -> t
 end
 
 module Make :