From 398fe8ee23759a1c28d91204aa013beae1dc602b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 12 Oct 2018 18:25:18 +0200 Subject: Cleaning the status of Local Definition and similar. Formerly, knowing if a declaration was to be discharged, to be global but invisible at import, or to be global but visible at import was obtained by combining the parser-level information (i.e. use of Variable/Hypothesis/Let vs use of Axiom/Parameter/Definition/..., use of Local vs Global) with the result of testing whether there were open sections. We change the meaning of the Discharge flag: it does not tell anymore that it was syntactically a Variable/Hypothesis/Let, but tells the expected semantics of the declaration (issuing a warning in the parser-to-interpreter step if the semantics is not the one suggested by the syntax). In particular, the interpretation/command engine becomes independent of the parser. The new "semantic" type is: type import_status = ImportDefaultBehavior | ImportNeedQualified type locality = Discharge | Global of import_status In the process, we found a couple of inconsistencies in the treatment of the locality status. See bug #8722 and test file LocalDefinition.v. --- doc/plugin_tutorial/tuto1/src/simple_declare.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/plugin_tutorial/tuto1/src') diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 1e582e6456..eb8161c2bb 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -7,7 +7,7 @@ let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = DeclareDef.declare_definition ident k ce ubinders imps ?hook_data let declare_definition ~poly ident sigma body = - let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in + let k = Decl_kinds.(Global ImportDefaultBehavior, poly, Definition) in let udecl = UState.default_univ_decl in edeclare ident k ~opaque:false sigma udecl body None [] -- cgit v1.2.3