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.
---
 plugins/derive/derive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/derive')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 9c1882dc9a..7c0f269481 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -26,7 +26,7 @@ let start_deriving f suchthat lemma =
 
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in
+  let kind = Decl_kinds.(Global ImportDefaultBehavior,false,DefinitionBody Definition) in
 
   (* create a sort variable for the type of [f] *)
   (* spiwack: I don't know what the rigidity flag does, picked the one
-- 
cgit v1.2.3