[declare] Remove superfluous API

`declare_definition` didn't improve a lot the declare path and was
used only once on interesting code. Also, it had many optional
parameters. The declare path is critical enough as to care about a
tidy API.

3 files changed, 6 insertions, 18 deletions

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 1e87a4b6ac..bfea15ac16 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -290,13 +290,6 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
   let eff = { Evd.seff_private = eff; Evd.seff_roles; } in
   kn, eff
 
-let declare_definition
-  ?(opaque=false) ?(kind=Decls.Definition) ?(local = ImportDefaultBehavior)
-  ~name ?types (body,univs) =
-  let cb = definition_entry ?types ~univs ~opaque body in
-  declare_constant ~local ~name ~kind:Decls.(IsDefinition kind)
-    (DefinitionEntry cb)
-
 (** Declaration of section variables and local definitions *)
 type section_variable_entry =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
diff --git a/tactics/declare.mli b/tactics/declare.mli
index ae5c93db6a..93bb582751 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -70,15 +70,6 @@ val declare_private_constant
   -> Evd.side_effects constant_entry
   -> Constant.t * Evd.side_effects
 
-val declare_definition
-  :  ?opaque:bool
-  -> ?kind:Decls.definition_object_kind
-  -> ?local:import_status
-  -> name:Id.t
-  -> ?types:constr
-  -> constr Entries.in_universes_entry
-  -> Constant.t
-
 (** Since transparent constants' side effects are globally declared, we
  *  need that *)
 val set_declare_scheme :
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 90c43a1cb4..8d1c536db6 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1315,12 +1315,16 @@ let project_hint ~poly pri l2r r =
   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 id =
+  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 c = Declare.declare_definition ~name:id (c,ctx) 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 (Globnames.ConstRef c))