Added a Local Definition vernacular command. This type of definition

has to be refered through its qualified name even when the module
containing it is imported.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16263 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 41 insertions, 15 deletions

diff --git a/library/kindops.ml b/library/kindops.ml
index 35aebc531..6e6c7527b 100644
--- a/library/kindops.ml
+++ b/library/kindops.ml
@@ -24,18 +24,44 @@ let string_of_theorem_kind = function
   | Corollary -> "Corollary"
 
 let string_of_definition_kind def =
-  match def with
-  | Local, Coercion -> "Coercion Local"
-  | Global, Coercion -> "Coercion"
-  | Local, Definition -> "Let"
-  | Global, Definition -> "Definition"
-  | Local, SubClass -> "Local SubClass"
-  | Global, SubClass -> "SubClass"
-  | Global, CanonicalStructure -> "Canonical Structure"
-  | Global, Example -> "Example"
-  | Local, (CanonicalStructure|Example) ->
-      Errors.anomaly (Pp.str "Unsupported local definition kind")
-  | Local, Instance -> "Instance"
-  | Global, Instance -> "Global Instance"
-  | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method)
-      -> Errors.anomaly (Pp.str "Internal definition kind")
+  let (locality, kind) = def in
+  let error () = Errors.anomaly (Pp.str "Internal definition kind") in
+  match kind with
+  | Definition ->
+    begin match locality with
+    | Discharge -> "Let"
+    | Local -> "Local Definition"
+    | Global -> "Definition"
+    end
+  | Example ->
+    begin match locality with
+    | Discharge -> error ()
+    | Local -> "Local Example"
+    | Global -> "Example"
+    end
+  | Coercion ->
+    begin match locality with
+    | Discharge -> error ()
+    | Local -> "Local Coercion"
+    | Global -> "Coercion"
+    end
+  | SubClass ->
+    begin match locality with
+    | Discharge -> error ()
+    | Local -> "Local SubClass"
+    | Global -> "SubClass"
+    end
+  | CanonicalStructure ->
+    begin match locality with
+    | Discharge -> error ()
+    | Local -> error ()
+    | Global -> "Canonical Structure"
+    end
+  | Instance ->
+    begin match locality with
+    | Discharge -> error ()
+    | Local -> "Instance"
+    | Global -> "Global Instance"
+    end
+  | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
+    Errors.anomaly (Pp.str "Internal definition kind")