DeclareDef: Reorganizing declaration of definitions in a more structured way.

In particular, we highlight the similarities and differences between
local and global definitions.

1 files changed, 11 insertions, 23 deletions

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 7426c128cc..35fb18e292 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -33,34 +33,22 @@ let get_locality id ~kind = function
 | Local -> true
 | Global -> false
 
-let declare_global_definition ident ce local k pl imps =
-  let local = get_locality ident ~kind:"definition" local in
-  let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
-  let gr = ConstRef kn in
-  let () = maybe_declare_manual_implicits false gr imps in
-  let () = Declare.declare_univ_binders gr pl in
-  let () = definition_message ident in
-  gr
-
 let declare_definition ident (local, p, k) ce pl imps hook =
   let fix_exn = Future.fix_exn_of ce.const_entry_body in
-  let r = match local with
+  let gr = match local with
   | Discharge when Lib.sections_are_opened () ->
-    let c = SectionLocalDef ce in
-    let _ = declare_variable ident (Lib.cwd(), c, IsDefinition k) in
-    let () = definition_message ident in
-    let gr = VarRef ident in
-    let () = maybe_declare_manual_implicits false gr imps in
-    let () = Declare.declare_univ_binders gr pl in
-    let () = if Proof_global.there_are_pending_proofs () then
-	       warn_definition_not_visible ident
-    in
-    gr
+      let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in
+      let () = if Proof_global.there_are_pending_proofs () then warn_definition_not_visible ident in
+      VarRef ident
   | Discharge | Local | Global ->
-    declare_global_definition ident ce local k pl imps in
-  Lemmas.call_hook fix_exn hook local r; r
+      let local = get_locality ident ~kind:"definition" local in
+      let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
+      ConstRef kn in
+  let () = maybe_declare_manual_implicits false gr imps in
+  let () = Declare.declare_univ_binders gr pl in
+  let () = definition_message ident in
+  Lemmas.call_hook fix_exn hook local gr; gr
 
 let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
   declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ _ -> ()))
-