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.

1 files changed, 53 insertions, 0 deletions

diff --git a/test-suite/success/LocalDefinition.v b/test-suite/success/LocalDefinition.v
new file mode 100644
index 0000000000..22fb09526d
--- /dev/null
+++ b/test-suite/success/LocalDefinition.v
@@ -0,0 +1,53 @@
+(* Test consistent behavior of Local Definition (#8722) *)
+
+(* Test consistent behavior of Local Definition wrt Admitted *)
+
+Module TestAdmittedVisibility.
+  Module A.
+    Let a1 : nat. Admitted. (* Suppose to behave like a "Local Definition" *)
+    Local Definition b1 : nat. Admitted. (* Told to be a "Local Definition" *)
+    Local Definition c1 := 0.
+    Local Parameter d1 : nat.
+    Section S.
+      Let a2 : nat. Admitted. (* Told to be turned into a toplevel assumption *)
+      Local Definition b2 : nat. Admitted. (* Told to be a "Local Definition" *)
+      Local Definition c2 := 0.
+      Local Parameter d2 : nat.
+    End S.
+  End A.
+  Import A.
+  Fail Check a1. (* used to be accepted *)
+  Fail Check b1. (* used to be accepted *)
+  Fail Check c1.
+  Fail Check d1.
+  Fail Check a2. (* used to be accepted *)
+  Fail Check b2. (* used to be accepted *)
+  Fail Check c2.
+  Fail Check d2.
+End TestAdmittedVisibility.
+
+(* Test consistent behavior of Local Definition wrt automatic declaration of instances *)
+
+Module TestVariableAsInstances.
+  Module Test1.
+    Set Typeclasses Axioms Are Instances.
+    Class U.
+    Local Parameter b : U.
+    Definition testU := _ : U. (* _ resolved *)
+
+    Class T.
+    Variable a : T.  (* warned to be the same as "Local Parameter" *)
+    Definition testT := _ : T. (* _ resolved *)
+  End Test1.
+
+  Module Test2.
+    Unset Typeclasses Axioms Are Instances.
+    Class U.
+    Local Parameter b : U.
+    Fail Definition testU := _ : U. (* _ unresolved *)
+
+    Class T.
+    Variable a : T.  (* warned to be the same as "Local Parameter" thus should not be an instance *)
+    Fail Definition testT := _ : T. (* used to succeed *)
+  End Test2.
+End TestVariableAsInstances.