[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...

4 files changed, 15 insertions, 15 deletions

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 07f578d2a8..9366c4250d 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -218,7 +218,7 @@ let build_functional_principle (sigma : Evd.evar_map) old_princ_type sorts funs
     Declare.build_by_tactic env ~uctx ~poly:false ~typ ftac
   in
   (* uctx was ignored before *)
-  let hook = DeclareDef.Hook.make (hook new_principle_type) in
+  let hook = Declare.Hook.make (hook new_principle_type) in
   (body, typ, univs, hook, sigma)
 
 let change_property_sort evd toSort princ princName =
@@ -318,8 +318,8 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts
     let uctx = Evd.evar_universe_context sigma in
     let entry = Declare.definition_entry ~univs ?types body in
     let (_ : Names.GlobRef.t) =
-      DeclareDef.declare_entry ~name:new_princ_name ~hook
-        ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+      Declare.declare_entry ~name:new_princ_name ~hook
+        ~scope:(Declare.Global Declare.ImportDefaultBehavior)
         ~kind:Decls.(IsProof Theorem)
         ~impargs:[] ~uctx entry
     in
@@ -400,7 +400,7 @@ let register_struct is_rec fixpoint_exprl =
           Pp.(str "Body of Function must be given")
     in
     ComDefinition.do_definition ~name:fname.CAst.v ~poly:false
-      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+      ~scope:(Declare.Global Declare.ImportDefaultBehavior)
       ~kind:Decls.Definition univs binders None body (Some rtype);
     let evd, rev_pconstants =
       List.fold_left
@@ -419,7 +419,7 @@ let register_struct is_rec fixpoint_exprl =
     (None, evd, List.rev rev_pconstants)
   | _ ->
     ComFixpoint.do_fixpoint
-      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false
+      ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~poly:false
       fixpoint_exprl;
     let evd, rev_pconstants =
       List.fold_left
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ffb9a7e69b..5c82ed38bb 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1483,7 +1483,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
     let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
     Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None
   in
-  let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in
+  let info = Lemmas.Info.make ~hook:(Declare.Hook.make hook) () in
   let lemma =
     Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info sigma gls_type
   in
@@ -1721,7 +1721,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
   let tcc_lemma_name = add_suffix function_name "_tcc" in
   let tcc_lemma_constr = ref Undefined in
   (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
-  let hook {DeclareDef.Hook.S.uctx; _} =
+  let hook {Declare.Hook.S.uctx; _} =
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref =
       declare_f function_name Decls.(IsProof Lemma) arg_types term_ref
@@ -1767,5 +1767,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
         functional_ref
         (EConstr.of_constr rec_arg_type)
         relation rec_arg_num term_id using_lemmas (List.length res_vars) evd
-        (DeclareDef.Hook.make hook))
+        (Declare.Hook.make hook))
     ()
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 5baa23b3e9..aef5f645f4 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -342,7 +342,7 @@ GRAMMAR EXTEND Gram
   hint:
     [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
         tac = Pltac.tactic ->
-        { ComHints.HintsExtern (n,c, in_tac tac) } ] ]
+        { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ]
   ;
   operconstr: LEVEL "0"
     [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3834b21a14..3b8fb48eb0 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1894,10 +1894,10 @@ let declare_projection name instance_id r =
     in it_mkProd_or_LetIn ccl ctx
   in
   let types = Some (it_mkProd_or_LetIn typ ctx) in
-  let kind, opaque, scope = Decls.(IsDefinition Definition), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+  let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in
   let impargs, udecl = [], UState.default_univ_decl in
   let _r : GlobRef.t =
-    DeclareDef.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
+    Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
   in ()
 
 let build_morphism_signature env sigma m =
@@ -1961,10 +1961,10 @@ let add_morphism_as_parameter atts m n : unit =
   let env = Global.env () in
   let evd = Evd.from_env env in
   let poly = atts.polymorphic in
-  let kind, opaque, scope = Decls.(IsAssumption Logical), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+  let kind, opaque, scope = Decls.(IsAssumption Logical), false, Declare.Global Declare.ImportDefaultBehavior in
   let impargs, udecl = [], UState.default_univ_decl in
   let evd, types = build_morphism_signature env evd m in
-  let evd, pe = DeclareDef.prepare_parameter ~poly ~udecl ~types evd in
+  let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in
   let cst = Declare.declare_constant ~name:instance_id ~kind (Declare.ParameterEntry pe) in
   let cst = GlobRef.ConstRef cst in
   Classes.add_instance
@@ -1981,7 +1981,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let poly = atts.polymorphic in
   let kind = Decls.(IsDefinition Instance) in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
-  let hook { DeclareDef.Hook.S.dref; _ } = dref |> function
+  let hook { Declare.Hook.S.dref; _ } = dref |> function
     | GlobRef.ConstRef cst ->
       Classes.add_instance (Classes.mk_instance
                       (PropGlobal.proper_class env evd) Hints.empty_hint_info
@@ -1989,7 +1989,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
       declare_projection n instance_id (GlobRef.ConstRef cst)
     | _ -> assert false
   in
-  let hook = DeclareDef.Hook.make hook in
+  let hook = Declare.Hook.make hook in
   let info = Lemmas.Info.make ~hook ~kind () in
   Flags.silently
     (fun () ->