From 5196ab8da3416bb7ebd17c1445afe7f08ab01cae Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 20 Aug 2019 19:57:17 +0200
Subject: [declare] Use entry constructor instead of low-level record.

Non-delayed entries can be done with the current constructor, delayed
ones will require more work.
---
 vernac/declareObl.ml | 14 ++------------
 1 file changed, 2 insertions(+), 12 deletions(-)

(limited to 'vernac/declareObl.ml')

diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 9c8213ad8a..e3cffa8523 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -149,18 +149,8 @@ let declare_obligation prg obl body ty uctx =
       if get_shrink_obligations () && not poly then shrink_body body ty
       else ([], body, ty, [||])
     in
-    let body =
-      ((body, Univ.ContextSet.empty), Evd.empty_side_effects)
-    in
-    let ce =
-      { Declare.proof_entry_body = Future.from_val ~fix_exn:(fun x -> x) body
-      ; proof_entry_secctx = None
-      ; proof_entry_type = ty
-      ; proof_entry_universes = uctx
-      ; proof_entry_opaque = opaque
-      ; proof_entry_inline_code = false
-      ; proof_entry_feedback = None }
-    in
+    let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in
+
     (* ppedrot: seems legit to have obligations as local *)
     let constant =
       Declare.declare_constant ~name:obl.obl_name
-- 
cgit v1.2.3