4 files changed, 41 insertions, 7 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 786760122a..7b5be4c1c5 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -28,7 +28,6 @@ open Termops
 open Inductiveops
 open Typing
 open Decl_kinds
-open Vernacexpr
 open Typeclasses
 open Pattern
 open Patternops
@@ -156,6 +155,24 @@ 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 reference
+  | HintsConstr of Constrexpr.constr_expr
+
+type hint_mode =
+  | ModeInput (* No evars *)
+  | ModeNoHeadEvar (* No evar at the head *)
+  | ModeOutput (* Anything *)
+
+type hints_expr =
+  | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list
+  | HintsImmediate of reference_or_constr list
+  | HintsUnfold of reference list
+  | HintsTransparency of reference list * bool
+  | HintsMode of reference * hint_mode list
+  | HintsConstructors of reference list
+  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
+
 type import_level = [ `LAX | `WARN | `STRICT ]
 
 let warn_hint : import_level ref = ref `LAX
@@ -1326,7 +1343,7 @@ let interp_hints poly =
       let _, tacexp = Genintern.generic_intern env tacexp in
       HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
 
-let add_hints local dbnames0 h =
+let add_hints ~local dbnames0 h =
   if String.List.mem "nocore" dbnames0 then
     user_err Pp.(str "The hint database \"nocore\" is meant to stay empty.");
   let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index c7de10a2a5..f059887031 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -18,7 +18,6 @@ open Misctypes
 open Tactypes
 open Clenv
 open Pattern
-open Vernacexpr
 
 (** {6 General functions. } *)
 
@@ -71,6 +70,24 @@ type search_entry
 
 type hint_entry
 
+type reference_or_constr =
+  | HintsReference of Libnames.reference
+  | HintsConstr of Constrexpr.constr_expr
+
+type hint_mode =
+  | ModeInput (* No evars *)
+  | ModeNoHeadEvar (* No evar at the head *)
+  | ModeOutput (* Anything *)
+
+type hints_expr =
+  | HintsResolve of (Typeclasses.hint_info_expr * bool * reference_or_constr) list
+  | HintsImmediate of reference_or_constr list
+  | HintsUnfold of Libnames.reference list
+  | HintsTransparency of Libnames.reference list * bool
+  | HintsMode of Libnames.reference * hint_mode list
+  | HintsConstructors of Libnames.reference 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
@@ -178,7 +195,7 @@ val current_pure_db : unit -> hint_db list
 
 val interp_hints : polymorphic -> hints_expr -> hints_entry
 
-val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
+val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit
 
 val prepare_hint : bool (* Check no remaining evars *) ->
   (bool * bool) (* polymorphic or monomorphic, local or global *) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a42e4b44b5..bb57e2bf4f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -128,14 +128,14 @@ let unsafe_intro env store decl b =
     (sigma, mkNamedLambda_or_LetIn decl ev)
   end
 
-let introduction ?(check=true) id =
+let introduction id =
   Proofview.Goal.enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
     let hyps = named_context_val (Proofview.Goal.env gl) in
     let store = Proofview.Goal.extra gl in
     let env = Proofview.Goal.env gl in
-    let () = if check && mem_named_context_val id hyps then
+    let () = if mem_named_context_val id hyps then
       user_err ~hdr:"Tactics.introduction"
         (str "Variable " ++ Id.print id ++ str " is already declared.")
     in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index ddf78b1d4e..b17330f133 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -34,7 +34,7 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool
 
 (** {6 Primitive tactics. } *)
 
-val introduction    : ?check:bool -> Id.t -> unit Proofview.tactic
+val introduction    : Id.t -> unit Proofview.tactic
 val convert_concl   : ?check:bool -> types -> cast_kind -> unit Proofview.tactic
 val convert_hyp     : ?check:bool -> named_declaration -> unit Proofview.tactic
 val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic