Imported Upstream version 8.6

1 files changed, 0 insertions, 676 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
deleted file mode 100644
index 568b1d17..00000000
--- a/tactics/eauto.ml4
+++ /dev/null
@@ -1,676 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
-open Pp
-open Errors
-open Util
-open Names
-open Nameops
-open Term
-open Termops
-open Proof_type
-open Tacticals
-open Tacmach
-open Tactics
-open Patternops
-open Clenv
-open Auto
-open Genredexpr
-open Tacexpr
-open Misctypes
-open Locus
-open Locusops
-open Hints
-
-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_unsafe_type_of gl c) and t2 = pf_concl gl in
-  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)
-
-let e_assumption gl =
-  tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl
-
-TACTIC EXTEND eassumption
-| [ "eassumption" ] -> [ Proofview.V82.tactic e_assumption ]
-END
-
-TACTIC EXTEND eexact
-| [ "eexact" constr(c) ] -> [ Proofview.V82.tactic (e_give_exact c) ]
-END
-
-let registered_e_assumption gl =
-  tclFIRST (List.map (fun id gl -> e_give_exact (mkVar id) gl)
-              (pf_ids_of_hyps gl)) 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 =
-  [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 =
-  if n <= 0 then error "prolog - failure";
-  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 (fun x -> out_term (pf_apply (prepare_hint false (false,true)) gl x)) l in
-  let n =
-    match n with
-      | ArgArg n -> n
-      | _ -> error "Prolog called with a non closed argument."
-  in
-  try (prolog l n gl)
-  with UserError ("Refiner.tclFIRST",_) ->
-    errorlabstrm "Prolog.prolog" (str "Prolog failed.")
-
-TACTIC EXTEND prolog
-| [ "prolog" "[" open_constr_list(l) "]" int_or_var(n) ] -> [ Proofview.V82.tactic (prolog_tac l n) ]
-END
-
-open Auto
-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,_) -> Int.equal pr 0) l)
-			  
-let unify_e_resolve poly flags (c,clenv) =
-  Proofview.Goal.nf_enter begin
-      fun gl ->
-      let clenv', c = connect_hint_clenv poly c clenv gl in
-      Proofview.V82.tactic
-	(fun gls ->
-	 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 c)) gls)
-    end
-
-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 (c, _, _) = c in
-  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 (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
-          (e_trivial_fail_db db_list
-	      (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) ::
-    (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
-  in
-    tclFIRST (List.map tclCOMPLETE tacl) goal
-
-and e_my_find_search db_list local_db hdc concl =
-  let hint_of_db = hintmap_of hdc concl in
-  let hintl =
-      List.map_append (fun db ->
-	let flags = auto_flags_of_state (Hint_db.transparent_state db) in
-	  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}) ->
-      let b = match Hints.repr_hint t with
-      | Unfold_nth _ -> 1
-      | _ -> b
-      in
-      (b,
-        let tac = function
-        | Res_pf (term,cl) -> unify_resolve poly st (term,cl)
-        | ERes_pf (term,cl) -> 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 (Proofview.V82.of_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
-       let tac = Proofview.V82.of_tactic (run_hint t tac) in
-       (tac, lazy (pr_hint t)))
-  in
-  List.map tac_of_hint hintl
-
-and e_trivial_resolve db_list local_db gl =
-  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 =
-  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
-
-(*s The following module [SearchProblem] is used to instantiate the generic
-    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;
-  dblist : hint_db list;
-  localdb :  hint_db list;
-  prev : prev_search_state;
-  local_lemmas : Evd.open_constr list;
-}
-
-and prev_search_state = (* for info eauto *)
-  | Unknown
-  | Init
-  | State of search_state
-
-module SearchProblem = struct
-
-  type state = search_state
-
-  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 filter_tactics glls l =
-(*     let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *)
-(*     let evars = Evarutil.nf_evars (Refiner.project glls) in *)
-(*     msg (str"Goal:" ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *)
-    let rec aux = function
-      | [] -> []
-      | (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, cost, pptac) :: aux tacl
-	  with e when Errors.noncritical e ->
-            let e = Errors.push e in
-            Refiner.catch_failerror e; aux tacl
-    in aux l
-
-  (* Ordering of states is lexicographic on depth (greatest first) then
-     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 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
-      []
-    else
-      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);
-      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 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; local_lemmas = s.local_lemmas}) 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, 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 (pf_env g') (project g')
-		  hintl (List.hd s.localdb) in
-	     { depth = s.depth; priority = cost; tacres = lgls;
-	       last_tactic = pp; dblist = s.dblist;
-	       localdb = ldb :: List.tl s.localdb; prev = ps;
-               local_lemmas = s.local_lemmas})
-	  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, cost, pp) ->
-	     let nbgl' = List.length (sig_it lgls) in
-	     if nbgl' < nbgl then
-	       { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp;
-                  prev = ps; dblist = s.dblist; localdb = List.tl s.localdb;
-                  local_lemmas = s.local_lemmas }
-	     else
-	       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 s.local_lemmas)
-		     (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls))
-	       in
-		 { depth = pred s.depth; priority = cost; tacres = lgls;
-		   dblist = s.dblist; last_tactic = pp; prev = ps;
-		   localdb = newlocal @ List.tl s.localdb;
-                   local_lemmas = s.local_lemmas })
-	  l
-      in
-      List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
-
-  let pp s = hov 0 (str " depth=" ++ int s.depth ++ spc () ++
-		      (Lazy.force s.last_tactic))
-
-end
-
-module Search = Explore.Make(SearchProblem)
-
-(** Utilities for debug eauto / info eauto *)
-
-let global_debug_eauto = ref false
-let global_info_eauto = ref false
-
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optsync  = true;
-      Goptions.optdepr  = false;
-      Goptions.optname  = "Debug Eauto";
-      Goptions.optkey   = ["Debug";"Eauto"];
-      Goptions.optread  = (fun () -> !global_debug_eauto);
-      Goptions.optwrite = (:=) global_debug_eauto }
-
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optsync  = true;
-      Goptions.optdepr  = false;
-      Goptions.optname  = "Info Eauto";
-      Goptions.optkey   = ["Info";"Eauto"];
-      Goptions.optread  = (fun () -> !global_info_eauto);
-      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
-  else Off
-
-let pr_info_nop = function
-  | Info -> msg_debug (str "idtac.")
-  | _ -> ()
-
-let pr_dbg_header = function
-  | Off -> ()
-  | Debug -> msg_debug (str "(* debug eauto : *)")
-  | Info -> msg_debug (str "(* info eauto : *)")
-
-let pr_info dbg s =
-  if dbg != Info then ()
-  else
-    let rec loop s =
-      match s.prev with
-	| Unknown | Init -> s.depth
-	| State sp ->
-	  let mindepth = loop sp in
-	  let indent = String.make (mindepth - sp.depth) ' ' in
-	  msg_debug (str indent ++ Lazy.force s.last_tactic ++ str ".");
-	  mindepth
-    in
-    ignore (loop s)
-
-(** Eauto main code *)
-
-let make_initial_state dbg n gl dblist localdb lems =
-  { depth = n;
-    priority = 0;
-    tacres = tclIDTAC gl;
-    last_tactic = lazy (mt());
-    dblist = dblist;
-    localdb = [localdb];
-    prev = if dbg == Info then Init else Unknown;
-    local_lemmas = lems;
-  }
-
-let e_search_auto debug (in_depth,p) lems db_list gl =
-  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
-    | (true,_) -> Search.depth_first
-    | (false,Debug) -> Search.debug_breadth_first
-    | (false,_) -> Search.breadth_first
-  in
-  try
-    pr_dbg_header d;
-    let s = tac (make_initial_state d p gl db_list local_db lems) in
-    pr_info d s;
-    s.tacres
-  with Not_found ->
-    pr_info_nop d;
-    error "eauto: search failed"
-
-(* 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)
-
-let eauto ?(debug=Off) np lems dbnames =
-  let db_list = make_db_list dbnames in
-  tclTRY (e_search_auto debug np lems db_list)
-
-let full_eauto ?(debug=Off) n lems gl =
-  let dbnames = current_db_names () 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
-  | None -> full_eauto ~debug np lems
-  | Some l -> eauto ~debug np lems l
-
-let make_depth = function
-  | None -> !default_search_depth
-  | Some (ArgArg d) -> d
-  | _ -> error "eauto called with a non closed argument."
-
-let make_dimension n = function
-  | None -> (true,make_depth n)
-  | Some (ArgArg d) -> (false,d)
-  | _ -> error "eauto called with a non closed argument."
-
-open Genarg
-
-(* Hint bases *)
-
-let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
-
-ARGUMENT EXTEND hintbases
-  TYPED AS preident_list_opt
-  PRINTED BY pr_hintbases
-| [ "with" "*" ] -> [ None ]
-| [ "with" ne_preident_list(l) ] -> [ Some l ]
-| [ ] -> [ Some [] ]
-END
-
-let pr_constr_coma_sequence prc _ _ =
-  prlist_with_sep pr_comma (fun (_,c) -> prc c)
-
-ARGUMENT EXTEND constr_coma_sequence
-  TYPED AS open_constr_list
-  PRINTED BY pr_constr_coma_sequence
-| [ open_constr(c) "," constr_coma_sequence(l) ] -> [ c::l ]
-| [ open_constr(c) ] -> [ [c] ]
-END
-
-let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using (fun (_,c) -> prc c)
-
-ARGUMENT EXTEND auto_using
-  TYPED AS open_constr_list
-  PRINTED BY pr_auto_using
-| [ "using" constr_coma_sequence(l) ] -> [ l ]
-| [ ] -> [ [] ]
-END
-
-TACTIC EXTEND eauto
-| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
-    hintbases(db) ] ->
-    [ Proofview.V82.tactic (gen_eauto (make_dimension n p) lems db) ]
-END
-
-TACTIC EXTEND new_eauto
-| [ "new" "auto" int_or_var_opt(n) auto_using(lems)
-    hintbases(db) ] ->
-    [ match db with
-      | None -> new_full_auto (make_depth n) lems
-      | Some l -> new_auto (make_depth n) lems l ]
-END
-
-TACTIC EXTEND debug_eauto
-| [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
-    hintbases(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) ] ->
-    [ 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) ] ->
-    [ Proofview.V82.tactic (gen_eauto (true, make_depth p) lems db) ]
-END
-
-let cons a l = a :: l
-
-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
-    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 (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
-
-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) 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 Id.Set.mem id ids ->
-	(match Environ.named_body id env with
-	| Some b -> true, b
-	| None -> false, c)
-    | 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 -> 
-		if done_ then done_, arg :: acc 
-		else match aux arg with
-		| true, arg' -> true, arg' :: acc
-		| false, arg' -> false, arg :: acc)
-		(false, []) args
-	    in 
-	      if done_ then true, mkApp (f, Array.of_list (List.rev args'))
-	      else false, c)
-    | _ -> 
-	let done_ = ref false in
-	let c' = map_constr (fun c -> 
-	  if !done_ then c else 
-	    let x, c' = aux c in
-	      done_ := x; c') c
-	in !done_, c'
-  in aux c
-
-let autounfold_one db cl =
-  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
-	(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
-    if did then
-      match cl with
-      | 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
-
-(* 	  Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts *)
-(* 	    (Id.Set.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) *)
-(*       in unfold_option unfolds cl *)
-
-(*       let db = try searchtable_map dbname  *)
-(* 	with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname) *)
-(*       in *)
-(*       let (ids, csts) = Hint_db.unfolds db in *)
-(* 	Cset.fold (fun cst -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cst)) csts *)
-(* 	  (Id.Set.fold (fun id -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cl) ids acc))) *)
-(*       (tclFAIL 0 (mt())) db *)
-      
-TACTIC EXTEND autounfold_one
-| [ "autounfold_one" hintbases(db) "in" hyp(id) ] ->
-    [ autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, InHyp)) ]
-| [ "autounfold_one" hintbases(db) ] ->
-    [ autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None ]
-      END
-
-TACTIC EXTEND autounfoldify
-| [ "autounfoldify" constr(x) ] -> [
-  Proofview.V82.tactic (
-    let db = match kind_of_term x with
-      | Const (c,_) -> Label.to_string (con_label c)
-      | _ -> assert false
-    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)  ] -> [
-    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
-      Tacticals.New.tclZEROMSG msg
-    | Some t ->
-      let state = Hint_db.transparent_state t in
-      unify ~state x y
-  ]
-END
-
-
-TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ]
-END
-
-let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom
-
-ARGUMENT EXTEND hints_path_atom
-  TYPED AS hints_path_atom
-  PRINTED BY pr_hints_path_atom
-| [ global_list(g) ] -> [ PathHints (List.map Nametab.global g) ]
-| [ "*" ] -> [ PathAny ]
-END
-
-let pr_hints_path prc prx pry c = Hints.pp_hints_path c
-
-ARGUMENT EXTEND hints_path
-  TYPED AS hints_path
-  PRINTED BY pr_hints_path
-| [ "(" hints_path(p) ")"  ] -> [ p ]
-| [ "!" hints_path(p)  ] -> [ PathStar p ]
-| [ "emp" ] -> [ PathEmpty ]
-| [ "eps" ] -> [ PathEpsilon ]
-| [ hints_path_atom(a) ] -> [ PathAtom a ]
-| [ hints_path(p) "|" hints_path(q) ] -> [ PathOr (p, q) ]
-| [ hints_path(p) ";" hints_path(q) ] -> [ PathSeq (p, q) ]
-END
-
-let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
-
-ARGUMENT EXTEND opthints
-  TYPED AS preident_list_opt
-  PRINTED BY pr_hintbases
-| [ ":" ne_preident_list(l) ] -> [ Some l ]
-| [ ] -> [ None ]
-END
-
-VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
-| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [
-  let entry = HintsCutEntry p in
-    Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
-      (match dbnames with None -> ["core"] | Some l -> l) entry ]
-END