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...
---
 vernac/comHints.mli | 20 +-------------------
 1 file changed, 1 insertion(+), 19 deletions(-)

(limited to 'vernac/comHints.mli')

diff --git a/vernac/comHints.mli b/vernac/comHints.mli
index 77fbef5387..20894eecf1 100644
--- a/vernac/comHints.mli
+++ b/vernac/comHints.mli
@@ -8,22 +8,4 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Typeclasses
-
-type hint_info_expr = Constrexpr.constr_pattern_expr 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
-
-val interp_hints : poly:bool -> hints_expr -> Hints.hints_entry
+val interp_hints : poly:bool -> Vernacexpr.hints_expr -> Hints.hints_entry
-- 
cgit v1.2.3