From 7d46a32dc928af64e3e111d6d62caa00f93c427c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 18 Mar 2020 05:35:41 -0400
Subject: [declare] Fuse prepare and declare for the non-interactive path.

This will allow to share the definition metadata for example with
obligations; a bit more work is needed to finally move the preparation
of interactive proofs from Proof_global to `prepare_entry`.
---
 plugins/funind/gen_principle.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index ebd280ecf6..45c46c56f4 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -290,13 +290,12 @@ let generate_functional_principle (evd: Evd.evar_map ref)
      Don't forget to close the goal if an error is raised !!!!
   *)
   let uctx = Evd.evar_universe_context sigma in
-  let entry = DeclareDef.ClosedDef.of_proof_entry ~uctx entry in
-  let _ : Names.GlobRef.t = DeclareDef.declare_definition
+  let _ : Names.GlobRef.t = DeclareDef.declare_entry
       ~name:new_princ_name ~hook
       ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
       ~kind:Decls.(IsProof Theorem)
       ~impargs:[]
-      entry in
+      ~uctx entry in
   ()
   with e when CErrors.noncritical e ->
     raise (Defining_principle e)
-- 
cgit v1.2.3