From 6675e7c54ae552df31a281098ba7f7d199372aec Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 1 May 2020 10:44:44 +0200
Subject: [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...
---
 plugins/funind/recdef.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/funind/recdef.ml')

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))
     ()
-- 
cgit v1.2.3