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, 11 insertions, 11 deletions

diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index e03c3e9b5..7cf60b7ff 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -123,18 +123,18 @@ let compute_name internal id =
 let define internal id c =
   let fd = declare_constant ~internal in
   let id = compute_name internal id in
-  let kn = fd id
-    (DefinitionEntry
-      { const_entry_body = c;
-        const_entry_secctx = None;
-        const_entry_type = None;
-        const_entry_opaque = false;
-	const_entry_inline_code = false
-      },
-      Decl_kinds.IsDefinition Scheme) in
-  (match internal with
+  let entry = {
+    const_entry_body = c;
+    const_entry_secctx = None;
+    const_entry_type = None;
+    const_entry_opaque = false;
+    const_entry_inline_code = false
+  } in
+  let kn = fd id (DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
+  let () = match internal with
   | KernelSilent -> ()
-  | _-> definition_message id);
+  | _-> definition_message id
+  in
   kn
 
 let define_individual_scheme_base kind suff f internal idopt (mind,i as ind) =