[declare] Merge DeclareDef into Declare

The API in `DeclareDef` should become the recommended API in `Declare`.

This greatly reduces the exposure of internals; we still have a large
offender in `Lemmas` but that will be taken care of in the next
commit; effectively removing quite some chunks from `declare.mli`.

This PR originally introduced a dependency cycle due to:

- `Declare`: uses `Vernacexpr.decl_notation list`
- `Vernacexpr`: uses `ComHint.hint_expr`
- `ComHint`: uses `Declare.declare_constant`

This is a real cycle in the sense that `ComHint` would have also move
to `DeclareDef` in the medium term.

There were quite a few ways to solve it, we have chosen to
move the hints ast to `Vernacexpr` as it is not very invasive
and seems consistent with the current style.

Alternatives, which could be considered at a later stage are for
example moving the notations AST to `Metasyntax`, having `Declare` not
to depend on `Vernacexpr` [which seems actually a good thing to do in
the medium term], reworking notation support more deeply...

1 files changed, 4 insertions, 21 deletions

diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 5a48e9c16c..2fd6fe2b29 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -13,23 +13,6 @@ open Util
 (** (Partial) implementation of the [Hint] command; some more
    functionality still lives in tactics/hints.ml *)
 
-type hint_info_expr = Constrexpr.constr_pattern_expr Typeclasses.hint_info_gen
-
-type reference_or_constr =
-  | HintsReference of Libnames.qualid
-  | HintsConstr of Constrexpr.constr_expr
-
-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.hints_transparency_target * bool
-  | HintsMode of Libnames.qualid * Hints.hint_mode list
-  | HintsConstructors of Libnames.qualid list
-  | HintsExtern of
-      int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
-
 let project_hint ~poly pri l2r r =
   let open EConstr in
   let open Coqlib in
@@ -108,6 +91,7 @@ let interp_hints ~poly h =
   let fr r = Tacred.evaluable_of_global_reference env (fref r) in
   let fi c =
     let open Hints in
+    let open Vernacexpr in
     match c with
     | HintsReference c ->
       let gr = Smartlocate.global_with_alias c in
@@ -126,15 +110,14 @@ let interp_hints ~poly h =
     in
     (info, poly, b, path, gr)
   in
-  let ft =
-    let open Hints in
-    function
+  let open Hints in
+  let open Vernacexpr 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
-  let open Hints in
   match h with
   | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
   | HintsResolveIFF (l2r, lc, n) ->