diff options
| author | Emilio Jesus Gallego Arias | 2020-05-01 10:44:44 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-07 18:13:56 +0200 |
| commit | 6675e7c54ae552df31a281098ba7f7d199372aec (patch) | |
| tree | 294a830870202c75d1bb44ab4e9c8630961a4576 /vernac/comFixpoint.mli | |
| parent | ad84e6948a86db491a00bb92ec3e00a9a743b1f9 (diff) | |
[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...
Diffstat (limited to 'vernac/comFixpoint.mli')
| -rw-r--r-- | vernac/comFixpoint.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index a19b96f0f3..bdb1ac19d4 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -16,16 +16,16 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint_interactive : - scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t + scope:Declare.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t val do_fixpoint : - scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit + scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit val do_cofixpoint_interactive : - scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t + scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t val do_cofixpoint : - scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit + scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit (************************************************************************) (** Internal API *) |