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 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'vernac/comAssumption.ml')

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