[hints] Move and split Hint Declaration AST to vernac

This moves the vernacular part of hints to `vernac`; in particular, it
helps removing the declaration of constants as parts of the `tactic`
folder.

2 files changed, 0 insertions, 143 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index ffb0e030db..0499ba200e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -23,7 +23,6 @@ open Globnames
 open Libobject
 open Namegen
 open Libnames
-open Smartlocate
 open Termops
 open Inductiveops
 open Typeclasses
@@ -100,8 +99,6 @@ let empty_hint_info =
 (*           The Type of Constructions Autotactic Hints                 *)
 (************************************************************************)
 
-type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
-
 type 'a hint_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
@@ -164,10 +161,6 @@ type full_hint = hint with_metadata
 type hint_entry = GlobRef.t option *
   raw_hint hint_ast with_uid with_metadata
 
-type reference_or_constr =
-  | HintsReference of qualid
-  | HintsConstr of Constrexpr.constr_expr
-
 type hint_mode =
   | ModeInput (* No evars *)
   | ModeNoHeadEvar (* No evar at the head *)
@@ -178,16 +171,6 @@ type 'a hints_transparency_target =
   | HintsConstants
   | HintsReferences of 'a list
 
-type hints_expr =
-  | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
-  | HintsResolveIFF of bool * qualid list * int option
-  | HintsImmediate of reference_or_constr list
-  | HintsUnfold of qualid list
-  | HintsTransparency of qualid hints_transparency_target * bool
-  | HintsMode of qualid * hint_mode list
-  | HintsConstructors of qualid list
-  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
-
 type import_level = HintLax | HintWarn | HintStrict
 
 let warn_hint_to_string = function
@@ -1310,114 +1293,6 @@ let prepare_hint check env init (sigma,c) =
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     (c', diff)
 
-let project_hint ~poly pri l2r r =
-  let open EConstr in
-  let open Coqlib in
-  let gr = Smartlocate.global_with_alias r in
-  let env = Global.env() in
-  let sigma = Evd.from_env env in
-  let sigma, c = Evd.fresh_global env sigma gr in
-  let t = Retyping.get_type_of env sigma c in
-  let t =
-    Tacred.reduce_to_quantified_ref env sigma (lib_ref "core.iff.type") t in
-  let sign,ccl = decompose_prod_assum sigma t in
-  let (a,b) = match snd (decompose_app sigma ccl) with
-    | [a;b] -> (a,b)
-    | _ -> assert false in
-  let p =
-    if l2r then lib_ref "core.iff.proj1" else lib_ref "core.iff.proj2" in
-  let sigma, p = Evd.fresh_global env sigma p in
-  let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
-  let c = it_mkLambda_or_LetIn
-    (mkApp (p,[|mkArrow a Sorts.Relevant (lift 1 b);mkArrow b Sorts.Relevant (lift 1 a);c|])) sign in
-  let name =
-    Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
-  in
-  let ctx = Evd.univ_entry ~poly sigma in
-  let c = EConstr.to_constr sigma c in
-  let cb = Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c)) in
-  let c = Declare.declare_constant
-      ~local:Declare.ImportDefaultBehavior
-      ~name ~kind:Decls.(IsDefinition Definition) cb
-  in
-  let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
-    (info,false,true,PathAny, IsGlobRef (GlobRef.ConstRef c))
-
-let warn_deprecated_hint_constr =
-  CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated"
-         (fun () ->
-           Pp.strbrk
-             "Declaring arbitrary terms as hints is deprecated; declare a global reference instead"
-         )
-
-let interp_hints ~poly =
-  fun h ->
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  let f poly c =
-    let evd,c = Constrintern.interp_open_constr env sigma c in
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    let (c, diff) = prepare_hint true env sigma (evd,c) in
-    if poly then IsConstr (c, diff)
-    else
-      let () = Declare.declare_universe_context ~poly:false diff in
-      IsConstr (c, Univ.ContextSet.empty)
-  in
-  let fref r =
-    let gr = global_with_alias r in
-    Dumpglob.add_glob ?loc:r.CAst.loc gr;
-    gr in
-  let fr r = evaluable_of_global_reference env (fref r) in
-  let fi c =
-    match c with
-    | HintsReference c ->
-      let gr = global_with_alias c in
-        (PathHints [gr], poly, IsGlobRef gr)
-    | HintsConstr c ->
-      let () = warn_deprecated_hint_constr () in
-      (PathAny, poly, f poly c)
-  in
-  let fp = Constrintern.intern_constr_pattern env sigma in
-  let fres (info, b, r) =
-    let path, poly, gr = fi r in
-    let info = { info with hint_pattern = Option.map fp info.hint_pattern } in
-      (info, poly, b, path, gr)
-  in
-  let ft = function
-    | HintsVariables -> HintsVariables
-    | HintsConstants -> HintsConstants
-    | HintsReferences lhints -> HintsReferences (List.map fr lhints)
-  in
-  let fp = Constrintern.intern_constr_pattern (Global.env()) in
-  match h with
-  | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
-  | HintsResolveIFF (l2r, lc, n) ->
-    HintsResolveEntry (List.map (project_hint ~poly n l2r) lc)
-  | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
-  | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints)
-  | HintsTransparency (t, b) -> HintsTransparencyEntry (ft t, b)
-  | HintsMode (r, l) -> HintsModeEntry (fref r, l)
-  | HintsConstructors lqid ->
-      let constr_hints_of_ind qid =
-        let ind = global_inductive_with_alias qid in
-        let mib,_ = Global.lookup_inductive ind in
-        Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind";
-          List.init (nconstructors env ind)
-            (fun i -> let c = (ind,i+1) in
-                      let gr = GlobRef.ConstructRef c in
-                        empty_hint_info,
-                        (Declareops.inductive_is_polymorphic mib), true,
-                        PathHints [gr], IsGlobRef gr)
-      in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
-  | HintsExtern (pri, patcom, tacexp) ->
-      let pat =	Option.map (fp sigma) patcom in
-      let l = match pat with None -> [] | Some (l, _) -> l in
-      let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
-      let env = Genintern.({ (empty_glob_sign env) with ltacvars }) in
-      let _, tacexp = Genintern.generic_intern env tacexp in
-      HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
-
 let add_hints ~locality dbnames h =
   let local, superglobal = match locality with
   | Goptions.OptDefault | Goptions.OptGlobal -> false, true
diff --git a/tactics/hints.mli b/tactics/hints.mli
index eed0e37fac..a54da8ef0a 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -32,8 +32,6 @@ val empty_hint_info : 'a Typeclasses.hint_info_gen
 
 (** Pre-created hint databases *)
 
-type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
-
 type 'a hint_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
@@ -78,10 +76,6 @@ type search_entry
 
 type hint_entry
 
-type reference_or_constr =
-  | HintsReference of Libnames.qualid
-  | HintsConstr of Constrexpr.constr_expr
-
 type hint_mode =
   | ModeInput (* No evars *)
   | ModeNoHeadEvar (* No evar at the head *)
@@ -92,16 +86,6 @@ type 'a hints_transparency_target =
   | HintsConstants
   | HintsReferences of 'a list
 
-type hints_expr =
-  | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
-  | HintsResolveIFF of bool * Libnames.qualid list * int option
-  | HintsImmediate of reference_or_constr list
-  | HintsUnfold of Libnames.qualid list
-  | HintsTransparency of Libnames.qualid hints_transparency_target * bool
-  | HintsMode of Libnames.qualid * hint_mode list
-  | HintsConstructors of Libnames.qualid list
-  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
-
 type 'a hints_path_gen =
   | PathAtom of 'a hints_path_atom_gen
   | PathStar of 'a hints_path_gen
@@ -217,8 +201,6 @@ val current_db_names : unit -> String.Set.t
 
 val current_pure_db : unit -> hint_db list
 
-val interp_hints : poly:bool -> hints_expr -> hints_entry
-
 val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_entry -> unit
 
 val prepare_hint : bool (* Check no remaining evars *) ->