From 4425c8d353ffdcbed966c253f9624b550626ae0a Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 11 Mar 2013 20:14:31 +0000
Subject: 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
---
 toplevel/ind_tables.ml | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'toplevel/ind_tables.ml')

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) =
-- 
cgit v1.2.3