[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, 4 deletions

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index bf38088f71..4e9e24b119 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -230,7 +230,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
       let name = add_suffix recname "_func" in
       (* XXX: Mutating the evar_map in the hook! *)
       (* XXX: Likely the sigma is out of date when the hook is called .... *)
-      let hook sigma { DeclareDef.Hook.S.dref; _ } =
+      let hook sigma { Declare.Hook.S.dref; _ } =
         let sigma, h_body = Evarutil.new_global sigma dref in
         let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in
         let ty = it_mkProd_or_LetIn top_arity binders_rel in
@@ -248,13 +248,13 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
       hook, name, typ
     else
       let typ = it_mkProd_or_LetIn top_arity binders_rel in
-      let hook sigma { DeclareDef.Hook.S.dref; _ } =
+      let hook sigma { Declare.Hook.S.dref; _ } =
         if Impargs.is_implicit_args () || not (List.is_empty impls) then
           Impargs.declare_manual_implicits false dref impls
       in hook, recname, typ
   in
   (* XXX: Capturing sigma here... bad bad *)
-  let hook = DeclareDef.Hook.make (hook sigma) in
+  let hook = Declare.Hook.make (hook sigma) in
   RetrieveObl.check_evars env sigma;
   let evars, _, evars_def, evars_typ =
     RetrieveObl.retrieve_obligations env recname sigma 0 def typ
@@ -290,7 +290,7 @@ let do_program_recursive ~scope ~poly fixkind fixl =
     let evars, _, def, typ =
       RetrieveObl.retrieve_obligations env name evm
         (List.length rec_sign) def typ in
-    ({ DeclareDef.Recthm.name; typ; impargs; args = [] }, def, evars)
+    ({ Declare.Recthm.name; typ; impargs; args = [] }, def, evars)
   in
   let (fixnames,fixrs,fixdefs,fixtypes) = fix in
   let fiximps = List.map pi2 info in