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... --- doc/plugin_tutorial/tuto1/src/simple_declare.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc/plugin_tutorial/tuto1/src/simple_declare.ml') diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index b94b1fc657..e9e866c5fb 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,6 +1,6 @@ let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in - let scope = DeclareDef.Global Declare.ImportDefaultBehavior in + let scope = Declare.Global Declare.ImportDefaultBehavior in let kind = Decls.(IsDefinition Definition) in - DeclareDef.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl + Declare.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl ~opaque:false ~poly ~types:None ~body sigma -- cgit v1.2.3