Merge branch 'v8.5'

9 files changed, 212 insertions, 152 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 45052685d..46274f832 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/class_tactics.ml b/tactics/class_tactics.ml
index 244f9a727..3fafbe15a 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -221,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 *)
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 789bcd1bd..607664486 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -172,18 +172,18 @@ and e_my_find_search db_list local_db hdc concl =
   let tac_of_hint =
     fun (st, {pri = b; pat = p; code = t; poly = poly}) ->
       (b,
-       let tac =
-	 match t with
-	   | 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) -> e_exact poly st (c,cl)
-	   | Res_pf_THEN_trivial_fail (term,cl) ->
-               (Tacticals.New.tclTHEN (Proofview.V82.tactic (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
+        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) -> e_exact poly st (c,cl)
+        | Res_pf_THEN_trivial_fail (term,cl) ->
+          Tacticals.New.tclTHEN (Proofview.V82.tactic (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 = run_auto_tactic t tac in
+       (tac, lazy (pr_autotactic t)))
   in
   List.map tac_of_hint hintl
 
@@ -194,7 +194,7 @@ and e_trivial_resolve db_list local_db gl =
 
 let e_possible_resolve db_list local_db gl =
   let hd = try Some (decompose_app_bound gl) with Bound -> None in
-  try List.map snd (e_my_find_search db_list local_db hd gl)
+  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 =
@@ -204,6 +204,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;
@@ -231,12 +232,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 (Proofview.V82.of_tactic 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
@@ -246,8 +247,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
@@ -258,42 +262,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 [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 [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
@@ -304,7 +305,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
@@ -373,6 +374,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;
@@ -576,7 +578,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/equality.ml b/tactics/equality.ml
index bcfd6657e..7ab8d0c3b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1493,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 =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 101223b57..dea47794e 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.create ();
+  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.create ()) 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)
 
@@ -411,34 +427,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
@@ -496,10 +516,12 @@ module Hint_db = struct
   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 +532,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 +553,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
 
@@ -782,10 +808,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 +824,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 +866,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 +898,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 +922,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 +965,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 +974,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 45cf562c0..958cca1c3 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/tacinterp.ml b/tactics/tacinterp.ml
index f894eb8fc..f29680e18 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2119,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
@@ -2138,9 +2143,13 @@ and interp_atomic ist tac : unit Proofview.tactic =
         Proofview.V82.tactic begin fun gl -> 
           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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b1559da33..7484139c6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -584,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
@@ -612,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
@@ -656,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)
@@ -2769,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
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index eea495621..0069d100b 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