From 6fe12fdac4acee36c99ea780d260ce5a9756cb1d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 3 Jun 2020 16:34:39 +0200
Subject: [declare] Hide internals of variable declaration entries.

In particular this avoids exposing `Evd.side_effects proof_entry` in
the API.
---
 vernac/comAssumption.ml |  3 +--
 vernac/declare.ml       |  7 +++++--
 vernac/declare.mli      | 10 ++--------
 3 files changed, 8 insertions(+), 12 deletions(-)

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 023d76ce3b..44c30598aa 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -24,8 +24,7 @@ module RelDecl = Context.Rel.Declaration
 
 let declare_variable is_coe ~kind typ imps impl {CAst.v=name} =
   let kind = Decls.IsAssumption kind in
-  let decl = Declare.SectionLocalAssum {typ; impl} in
-  let () = Declare.declare_variable ~name ~kind decl in
+  let () = Declare.declare_variable ~name ~kind ~typ ~impl in
   let () = Declare.assumption_message name in
   let r = GlobRef.VarRef name in
   let () = maybe_declare_manual_implicits true r imps in
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 6ed7a9e39d..7de1ff4083 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -554,7 +554,7 @@ let objVariable : unit Libobject.Dyn.tag =
 
 let inVariable v = Libobject.Dyn.Easy.inj v objVariable
 
-let declare_variable ~name ~kind d =
+let declare_variable_core ~name ~kind d =
   (* Variables are distinguished by only short names *)
   if Decls.variable_exists name then
     raise (DeclareUniv.AlreadyDeclared (None, name));
@@ -591,6 +591,9 @@ let declare_variable ~name ~kind d =
   Impargs.declare_var_implicits ~impl name;
   Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name)
 
+let declare_variable ~name ~kind ~typ ~impl =
+  declare_variable_core ~name ~kind (SectionLocalAssum { typ; impl })
+
 (* Declaration messages *)
 
 let pr_rank i = pr_nth (i+1)
@@ -913,7 +916,7 @@ let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry =
   let ubind = UState.universe_binders uctx in
   let dref = match scope with
   | Discharge ->
-    let () = declare_variable ~name ~kind (SectionLocalDef entry) in
+    let () = declare_variable_core ~name ~kind (SectionLocalDef entry) in
     if should_suggest then Proof_using.suggest_variable (Global.env ()) name;
     Names.GlobRef.VarRef name
   | Global local ->
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 5339f4702b..ef4f8c4825 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -116,13 +116,6 @@ val close_proof : opaque:opacity_flag -> keep_body_ucst_separate:bool -> Proof.t
 
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
-(** XXX: This is an internal, low-level API and could become scheduled
-   for removal from the public API, use higher-level declare APIs
-   instead *)
-type variable_declaration =
-  | SectionLocalDef of Evd.side_effects proof_entry
-  | SectionLocalAssum of { typ:types; impl:Glob_term.binding_kind; }
-
 (** XXX: This is an internal, low-level API and could become scheduled
    for removal from the public API, use higher-level declare APIs
    instead *)
@@ -134,7 +127,8 @@ type 'a constant_entry =
 val declare_variable
   :  name:variable
   -> kind:Decls.logical_kind
-  -> variable_declaration
+  -> typ:types
+  -> impl:Glob_term.binding_kind
   -> unit
 
 (** Declaration of global constructions
-- 
cgit v1.2.3