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`.
---
 vernac/declareDef.mli | 47 ++++++++++++++++++++++++++---------------------
 1 file changed, 26 insertions(+), 21 deletions(-)

(limited to 'vernac/declareDef.mli')

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 8f3db59ba9..3bc1e25f19 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -39,23 +39,39 @@ module Hook : sig
   val call : ?hook:t -> S.t -> unit
 end
 
-module ClosedDef : sig
-  type t
-
-  (* Don't use for non-interactive proofs *)
-  val of_proof_entry
-    : uctx:UState.t
-    -> Evd.side_effects Declare.proof_entry -> t
-end
+(** Declare an interactively-defined constant *)
+val declare_entry
+  :  name:Id.t
+  -> scope:locality
+  -> kind:Decls.logical_kind
+  -> ?hook:Hook.t
+  -> ?obls:(Id.t * Constr.t) list
+  -> impargs:Impargs.manual_implicits
+  -> uctx:UState.t
+  -> Evd.side_effects Declare.proof_entry
+  -> GlobRef.t
 
+(** Declares a non-interactive constant; [body] and [types] will be
+   normalized w.r.t. the passed [evar_map] [sigma]. Universes should
+   be handled properly, including minimization and restriction. Note
+   that [sigma] is checked for unresolved evars, thus you should be
+   careful not to submit open terms or evar maps with stale,
+   unresolved existentials *)
 val declare_definition
   :  name:Id.t
   -> scope:locality
   -> kind:Decls.logical_kind
+  -> opaque:bool
+  -> impargs:Impargs.manual_implicits
+  -> udecl:UState.universe_decl
   -> ?hook:Hook.t
   -> ?obls:(Id.t * Constr.t) list
-  -> impargs:Impargs.manual_implicits
-  -> ClosedDef.t
+  -> poly:bool
+  -> ?inline:bool
+  -> types:EConstr.t option
+  -> body:EConstr.t
+  -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
+  -> Evd.evar_map
   -> GlobRef.t
 
 val declare_assumption
@@ -97,17 +113,6 @@ val declare_mutually_recursive
   -> Recthm.t list
   -> Names.GlobRef.t list
 
-val prepare_definition
-  :  ?opaque:bool
-  -> ?inline:bool
-  -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
-  -> poly:bool
-  -> udecl:UState.universe_decl
-  -> types:EConstr.t option
-  -> body:EConstr.t
-  -> Evd.evar_map
-  -> ClosedDef.t
-
 val prepare_obligation
   :  ?opaque:bool
   -> ?inline:bool
-- 
cgit v1.2.3