1 files changed, 163 insertions, 109 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 144100c9..30c5e686 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -1,40 +1,42 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4deps: "grammar/grammar.cma" i*)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
 open Term
 open Termops
-open Sign
-open Reduction
 open Proof_type
-open Declarations
 open Tacticals
 open Tacmach
-open Evar_refiner
 open Tactics
-open Pattern
+open Patternops
 open Clenv
 open Auto
-open Glob_term
-open Hiddentac
+open Genredexpr
 open Tacexpr
+open Misctypes
+open Locus
+open Locusops
+open Hints
 
-let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state }
+DECLARE PLUGIN "eauto"
+
+let eauto_unif_flags = auto_flags_of_state full_transparent_state
 
 let e_give_exact ?(flags=eauto_unif_flags) c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in
-  if occur_existential t1 or occur_existential t2 then
-     tclTHEN (Clenvtac.unify ~flags t1) (exact_check c) gl
-  else exact_check c gl
+  if occur_existential t1 || occur_existential t2 then
+     tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
+  else Proofview.V82.of_tactic (exact_check c) gl
 
 let assumption id = e_give_exact (mkVar id)
 
@@ -42,11 +44,11 @@ let e_assumption gl =
   tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl
 
 TACTIC EXTEND eassumption
-| [ "eassumption" ] -> [ e_assumption ]
+| [ "eassumption" ] -> [ Proofview.V82.tactic e_assumption ]
 END
 
 TACTIC EXTEND eexact
-| [ "eexact" constr(c) ] -> [ e_give_exact c ]
+| [ "eexact" constr(c) ] -> [ Proofview.V82.tactic (e_give_exact c) ]
 END
 
 let registered_e_assumption gl =
@@ -57,10 +59,29 @@ let registered_e_assumption gl =
 (*   PROLOG tactic                                                      *)
 (************************************************************************)
 
+(*s Tactics handling a list of goals. *)
+
+(* first_goal : goal list sigma -> goal sigma *)
+
+let first_goal gls =
+  let gl = gls.Evd.it and sig_0 = gls.Evd.sigma in
+  if List.is_empty gl then error "first_goal";
+  { Evd.it = List.hd gl; Evd.sigma = sig_0; }
+
+(* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
+
+let apply_tac_list tac glls =
+  let (sigr,lg) = unpackage glls in
+  match lg with
+  | (g1::rest) ->
+      let gl = apply_sig_tac sigr tac g1 in
+      repackage sigr (gl@rest)
+  | _ -> error "apply_tac_list"
+
 let one_step l gl =
-  [Tactics.intro]
-  @ (List.map h_simplest_eapply (List.map mkVar (pf_ids_of_hyps gl)))
-  @ (List.map h_simplest_eapply l)
+  [Proofview.V82.of_tactic Tactics.intro]
+  @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) (List.map mkVar (pf_ids_of_hyps gl)))
+  @ (List.map (fun c -> Proofview.V82.of_tactic (Tactics.Simple.eapply c)) l)
   @ (List.map assumption (pf_ids_of_hyps gl))
 
 let rec prolog l n gl =
@@ -68,11 +89,15 @@ let rec prolog l n gl =
   let prol = (prolog l (n-1)) in
   (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
 
+let out_term = function
+  | IsConstr (c, _) -> c
+  | IsGlobRef gr -> fst (Universes.fresh_global_instance (Global.env ()) gr)
+
 let prolog_tac l n gl =
-  let l = List.map (prepare_hint (pf_env gl)) l in
+  let l = List.map (fun x -> out_term (pf_apply (prepare_hint false) gl x)) l in
   let n =
     match n with
-      |  ArgArg n -> n
+      | ArgArg n -> n
       | _ -> error "Prolog called with a non closed argument."
   in
   try (prolog l n gl)
@@ -80,7 +105,7 @@ let prolog_tac l n gl =
     errorlabstrm "Prolog.prolog" (str "Prolog failed.")
 
 TACTIC EXTEND prolog
-| [ "prolog" "[" open_constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ]
+| [ "prolog" "[" open_constr_list(l) "]" int_or_var(n) ] -> [ Proofview.V82.tactic (prolog_tac l n) ]
 END
 
 open Auto
@@ -90,17 +115,26 @@ open Unification
 (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
 (***************************************************************************)
 
-let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
-
-let unify_e_resolve flags (c,clenv) gls =
-  let clenv' = connect_clenv gls clenv in
-  let _ = clenv_unique_resolver ~flags clenv' gls in
-  h_simplest_eapply c gls
-
+let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
+
+let unify_e_resolve poly flags (c,clenv) gls =
+  let clenv', subst = if poly then Clenv.refresh_undefined_univs clenv 
+  else clenv, Univ.empty_level_subst in
+  let clenv' = connect_clenv gls clenv' in
+  let clenv' = clenv_unique_resolver ~flags clenv' gls in
+    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 e_exact poly flags (c,clenv) =
+  let clenv', subst = 
+    if poly then Clenv.refresh_undefined_univs clenv 
+    else clenv, Univ.empty_level_subst
+  in e_give_exact (* ~flags *) (Vars.subst_univs_level_constr subst c)
+    
 let rec e_trivial_fail_db db_list local_db goal =
   let tacl =
     registered_e_assumption ::
-    (tclTHEN Tactics.intro
+    (tclTHEN (Proofview.V82.of_tactic Tactics.intro)
        (function g'->
 	  let d = pf_last_hyp g' in
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
@@ -108,43 +142,35 @@ let rec e_trivial_fail_db db_list local_db goal =
 	      (Hint_db.add_list hintl local_db) g'))) ::
     (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
   in
-  tclFIRST (List.map tclCOMPLETE tacl) goal
+    tclFIRST (List.map tclCOMPLETE tacl) goal
 
 and e_my_find_search db_list local_db hdc concl =
-  let hdc = head_of_constr_reference hdc in
   let hintl =
     if occur_existential concl then
-      list_map_append (fun db ->
-	let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in
-	  List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
+      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_unif_flags with modulo_delta = 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_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)
   in
   let tac_of_hint =
-    fun (st, {pri=b; pat = p; code=t}) ->
+    fun (st, {pri = b; pat = p; code = t; poly = poly}) ->
       (b,
        let tac =
 	 match t with
-	   | Res_pf (term,cl) -> unify_resolve st (term,cl)
-	   | ERes_pf (term,cl) -> unify_e_resolve st (term,cl)
-	   | Give_exact (c) -> e_give_exact c
+	   | 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 st (term,cl))
+               tclTHEN (unify_e_resolve poly st (term,cl))
 		 (e_trivial_fail_db db_list local_db)
-	   | Unfold_nth c -> h_reduce (Unfold [all_occurrences_expr,c]) onConcl
-	   | Extern tacast -> conclPattern concl p tacast
+	   | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
+	   | Extern tacast -> Proofview.V82.of_tactic (conclPattern concl p tacast)
        in
        (tac,lazy (pr_autotactic t)))
-       (*i
-	 fun gls -> pPNL (pr_autotactic t); Format.print_flush ();
-                     try tac gls
-		     with e when Logic.catchable_exception(e) ->
-                            (Format.print_string "Fail\n";
-			     Format.print_flush ();
-			     raise e)
-       i*)
   in
   List.map tac_of_hint hintl
 
@@ -152,13 +178,13 @@ and e_trivial_resolve db_list local_db gl =
   try
     priority
       (e_my_find_search db_list local_db
-	 (fst (head_constr_bound gl)) gl)
+	 (decompose_app_bound gl) gl)
   with Bound | Not_found -> []
 
 let e_possible_resolve db_list local_db gl =
   try List.map snd
     (e_my_find_search db_list local_db
-	(fst (head_constr_bound gl)) gl)
+	(decompose_app_bound gl) gl)
   with Bound | Not_found -> []
 
 let find_first_goal gls =
@@ -171,8 +197,8 @@ type search_state = {
   depth : int; (*r depth of search before failing *)
   tacres : goal list sigma;
   last_tactic : std_ppcmds Lazy.t;
-  dblist : Auto.hint_db list;
-  localdb :  Auto.hint_db list;
+  dblist : hint_db list;
+  localdb :  hint_db list;
   prev : prev_search_state
 }
 
@@ -185,13 +211,9 @@ module SearchProblem = struct
 
   type state = search_state
 
-  let success s = (sig_it s.tacres) = []
+  let success s = List.is_empty (sig_it s.tacres)
 
-  let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl)
-
-  let pr_goals gls =
-    let evars = Evarutil.nf_evar_map (Refiner.project gls) in
-      prlist (pr_ev evars) (sig_it gls)
+(*   let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) *)
 
   let filter_tactics glls l =
 (*     let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
@@ -206,6 +228,7 @@ module SearchProblem = struct
 (* 	      msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")); *)
 	      (lgls,pptac) :: aux tacl
 	  with e when Errors.noncritical e ->
+            let e = Errors.push e in
             Refiner.catch_failerror e; aux tacl
     in aux l
 
@@ -214,13 +237,13 @@ module SearchProblem = struct
   let compare s s' =
     let d = s'.depth - s.depth in
     let nbgoals s = List.length (sig_it s.tacres) in
-    if d <> 0 then d else nbgoals s - nbgoals s'
+    if not (Int.equal d 0) then d else nbgoals s - nbgoals s'
 
   let branching s =
-    if s.depth = 0 then
+    if Int.equal s.depth 0 then
       []
     else
-      let ps = if s.prev = Unknown then Unknown else State s in
+      let ps = if s.prev == Unknown then Unknown else State s in
       let lg = s.tacres in
       let nbgl = List.length (sig_it lg) in
       assert (nbgl > 0);
@@ -249,7 +272,7 @@ module SearchProblem = struct
 	     { depth = s.depth; tacres = res;
 	       last_tactic = pp; dblist = s.dblist;
 	       localdb = ldb :: List.tl s.localdb; prev = ps })
-	  (filter_tactics s.tacres [Tactics.intro,lazy (str "intro")])
+	  (filter_tactics s.tacres [Proofview.V82.of_tactic Tactics.intro,lazy (str "intro")])
       in
       let rec_tacs =
 	let l =
@@ -262,10 +285,18 @@ module SearchProblem = struct
 	       { depth = s.depth; tacres = res; last_tactic = pp; prev = ps;
 		 dblist = s.dblist; localdb = List.tl s.localdb }
 	     else
-	       { depth = pred s.depth; tacres = res;
-		 dblist = s.dblist; last_tactic = pp; prev = ps;
-		 localdb =
-		   list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
+	       let newlocal = 
+		 let hyps = pf_hyps g in
+		   List.map (fun gl ->
+		     let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in
+		     let hyps' = pf_hyps gls in
+		       if hyps' == hyps then List.hd s.localdb
+		       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;
+		   dblist = s.dblist; last_tactic = pp; prev = ps;
+		   localdb = newlocal @ List.tl s.localdb })
 	  l
       in
       List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
@@ -301,8 +332,8 @@ let _ =
       Goptions.optwrite = (:=) global_info_eauto }
 
 let mk_eauto_dbg d =
-  if d = Debug || !global_debug_eauto then Debug
-  else if d = Info || !global_info_eauto then Info
+  if d == Debug || !global_debug_eauto then Debug
+  else if d == Info || !global_info_eauto then Info
   else Off
 
 let pr_info_nop = function
@@ -315,7 +346,7 @@ let pr_dbg_header = function
   | Info -> msg_debug (str "(* info eauto : *)")
 
 let pr_info dbg s =
-  if dbg <> Info then ()
+  if dbg != Info then ()
   else
     let rec loop s =
       match s.prev with
@@ -336,11 +367,11 @@ let make_initial_state dbg n gl dblist localdb =
     last_tactic = lazy (mt());
     dblist = dblist;
     localdb = [localdb];
-    prev = if dbg=Info then Init else Unknown;
+    prev = if dbg == Info then Init else Unknown;
   }
 
 let e_search_auto debug (in_depth,p) lems db_list gl =
-  let local_db = make_local_hint_db ~ts:full_transparent_state true lems gl in
+  let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:full_transparent_state true lems in
   let d = mk_eauto_dbg debug in
   let tac = match in_depth,d with
     | (true,Debug) -> Search.debug_depth_first
@@ -357,7 +388,8 @@ let e_search_auto debug (in_depth,p) lems db_list gl =
     pr_info_nop d;
     error "eauto: search failed"
 
-open Evd
+(* let e_search_auto_key = Profile.declare_profile "e_search_auto" *)
+(* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *)
 
 let eauto_with_bases ?(debug=Off) np lems db_list =
   tclTRY (e_search_auto debug np lems db_list)
@@ -368,8 +400,8 @@ let eauto ?(debug=Off) np lems dbnames =
 
 let full_eauto ?(debug=Off) n lems gl =
   let dbnames = current_db_names () in
-  let dbnames =  list_remove "v62" dbnames in
-  let db_list = List.map searchtable_map dbnames in
+  let dbnames =  String.Set.remove "v62" dbnames in
+  let db_list = List.map searchtable_map (String.Set.elements dbnames) in
   tclTRY (e_search_auto debug n lems db_list) gl
 
 let gen_eauto ?(debug=Off) np lems = function
@@ -422,7 +454,7 @@ END
 TACTIC EXTEND eauto
 | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    [ gen_eauto (make_dimension n p) lems db ]
+    [ Proofview.V82.tactic (gen_eauto (make_dimension n p) lems db) ]
 END
 
 TACTIC EXTEND new_eauto
@@ -436,64 +468,70 @@ END
 TACTIC EXTEND debug_eauto
 | [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    [ gen_eauto ~debug:Debug (make_dimension n p) lems db ]
+    [ Proofview.V82.tactic (gen_eauto ~debug:Debug (make_dimension n p) lems db) ]
 END
 
 TACTIC EXTEND info_eauto
 | [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
     hintbases(db) ] ->
-    [ gen_eauto ~debug:Info (make_dimension n p) lems db ]
+    [ Proofview.V82.tactic (gen_eauto ~debug:Info (make_dimension n p) lems db) ]
 END
 
 TACTIC EXTEND dfs_eauto
 | [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems)
       hintbases(db) ] ->
-    [ gen_eauto (true, make_depth p) lems db ]
+    [ Proofview.V82.tactic (gen_eauto (true, make_depth p) lems db) ]
 END
 
 let cons a l = a :: l
 
-let autounfolds db occs =
+let autounfolds db occs cls gl =
   let unfolds = List.concat (List.map (fun dbname -> 
     let db = try searchtable_map dbname 
       with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
     in
     let (ids, csts) = Hint_db.unfolds db in
-      Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts
-	(Idset.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db)
-  in unfold_option unfolds
+    let hyps = pf_ids_of_hyps gl in
+    let ids = Idset.filter (fun id -> List.mem id hyps) ids in
+      Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts
+	(Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db)
+  in unfold_option unfolds cls gl
 
 let autounfold db cls gl =
-  let cls = concrete_clause_of cls gl in
+  let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in
   let tac = autounfolds db in
   tclMAP (function
     | OnHyp (id,occs,where) -> tac occs (Some (id,where))
     | OnConcl occs -> tac occs None)
     cls gl
 
-open Extraargs
+let autounfold_tac db cls gl =
+  let dbs = match db with
+  | None -> String.Set.elements (current_db_names ())
+  | Some [] -> ["core"]
+  | Some l -> l
+  in
+  autounfold dbs  cls gl
 
 TACTIC EXTEND autounfold
-| [ "autounfold" hintbases(db) in_arg_hyp(id) ] ->
-    [ autounfold (match db with None -> Auto.current_db_names () | Some [] -> ["core"] | Some x -> x) 
-	(glob_in_arg_hyp_to_clause id) ]
+| [ "autounfold" hintbases(db) clause(cl) ] -> [ Proofview.V82.tactic (autounfold_tac db cl) ]
 END
 
 let unfold_head env (ids, csts) c = 
   let rec aux c = 
     match kind_of_term c with
-    | Var id when Idset.mem id ids ->
+    | Var id when Id.Set.mem id ids ->
 	(match Environ.named_body id env with
 	| Some b -> true, b
 	| None -> false, c)
-    | Const cst when Cset.mem cst csts ->
-	true, Environ.constant_value env cst
+    | Const (cst,u as c) when Cset.mem cst csts ->
+	true, Environ.constant_value_in env c
     | App (f, args) ->
 	(match aux f with
 	| true, f' -> true, Reductionops.whd_betaiota Evd.empty (mkApp (f', args))
 	| false, _ -> 
 	    let done_, args' = 
-	      array_fold_left_i (fun i (done_, acc) arg -> 
+	      Array.fold_left_i (fun i (done_, acc) arg -> 
 		if done_ then done_, arg :: acc 
 		else match aux arg with
 		| true, arg' -> true, arg' :: acc
@@ -511,24 +549,30 @@ let unfold_head env (ids, csts) c =
 	in !done_, c'
   in aux c
 
-let autounfold_one db cl gl =
+let autounfold_one db cl =
+  Proofview.Goal.nf_enter begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let concl = Proofview.Goal.concl gl in
   let st =
     List.fold_left (fun (i,c) dbname -> 
       let db = try searchtable_map dbname 
 	with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
       in
       let (ids, csts) = Hint_db.unfolds db in
-	(Idset.union ids i, Cset.union csts c)) (Idset.empty, Cset.empty) db
+	(Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db
+  in
+  let did, c' = unfold_head env st 
+    (match cl with Some (id, _) -> Tacmach.New.pf_get_hyp_typ id gl | None -> concl) 
   in
-  let did, c' = unfold_head (pf_env gl) st (match cl with Some (id, _) -> pf_get_hyp_typ gl id | None -> pf_concl gl) in
     if did then
       match cl with
-      | Some hyp -> change_in_hyp None c' hyp gl
-      | None -> convert_concl_no_check c' DEFAULTcast gl
-    else tclFAIL 0 (str "Nothing to unfold") gl
+      | Some hyp -> change_in_hyp None (fun sigma -> sigma, c') hyp
+      | None -> convert_concl_no_check c' DEFAULTcast
+    else Tacticals.New.tclFAIL 0 (str "Nothing to unfold")
+  end
 
 (* 	  Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts *)
-(* 	    (Idset.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) *)
+(* 	    (Id.Set.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) *)
 (*       in unfold_option unfolds cl *)
 
 (*       let db = try searchtable_map dbname  *)
@@ -536,7 +580,7 @@ let autounfold_one db cl gl =
 (*       in *)
 (*       let (ids, csts) = Hint_db.unfolds db in *)
 (* 	Cset.fold (fun cst -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cst)) csts *)
-(* 	  (Idset.fold (fun id -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cl) ids acc))) *)
+(* 	  (Id.Set.fold (fun id -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cl) ids acc))) *)
 (*       (tclFAIL 0 (mt())) db *)
       
 TACTIC EXTEND autounfold_one
@@ -548,16 +592,26 @@ TACTIC EXTEND autounfold_one
 
 TACTIC EXTEND autounfoldify
 | [ "autounfoldify" constr(x) ] -> [
+  Proofview.V82.tactic (
     let db = match kind_of_term x with
-      | Const c -> string_of_label (con_label c)
+      | Const (c,_) -> Label.to_string (con_label c)
       | _ -> assert false
-    in autounfold ["core";db] onConcl ]
+    in autounfold ["core";db] onConcl 
+  )]
 END
 
 TACTIC EXTEND unify
 | ["unify" constr(x) constr(y) ] -> [ unify x y ]
 | ["unify" constr(x) constr(y) "with" preident(base)  ] -> [
-    unify ~state:(Hint_db.transparent_state (searchtable_map base)) x y ]
+    let table = try Some (searchtable_map base) with Not_found -> None in
+    match table with
+    | None ->
+      let msg = str "Hint table " ++ str base ++ str " not found" in
+      Proofview.tclZERO (UserError ("", msg))
+    | Some t ->
+      let state = Hint_db.transparent_state t in
+      unify ~state x y
+  ]
 END
 
 
@@ -570,7 +624,7 @@ let pr_hints_path_atom prc _ _ a =
   match a with
   | PathAny -> str"."
   | PathHints grs ->
-    prlist_with_sep pr_spc Printer.pr_global grs
+    pr_sequence Printer.pr_global grs
 
 ARGUMENT EXTEND hints_path_atom
   TYPED AS hints_path_atom
@@ -610,9 +664,9 @@ ARGUMENT EXTEND opthints
 | [ ] -> [ None ]
 END
 
-VERNAC COMMAND EXTEND HintCut
+VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
 | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [
   let entry = HintsCutEntry p in
-    Auto.add_hints (Vernacexpr.use_section_locality ()) 
+    Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
       (match dbnames with None -> ["core"] | Some l -> l) entry ]
 END