High level functions to produce kernel entries from econstr.

2 files changed, 30 insertions, 0 deletions

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 74b59735a9..898de7b166 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -54,3 +54,23 @@ let declare_definition ident (local, p, k) ?hook ce pl imps =
 let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
   declare_definition f kind ce pl imps
+
+let check_definition_evars ~allow_evars sigma =
+  let env = Global.env () in
+  if not allow_evars then Pretyping.check_evars_are_solved env sigma
+
+let prepare_definition ~allow_evars ?opaque ?inline ~poly sigma udecl ~types ~body =
+  check_definition_evars ~allow_evars sigma;
+  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
+      sigma (fun nf -> nf body, Option.map nf types)
+  in
+  let univs = Evd.check_univ_decl ~poly sigma udecl in
+  sigma, definition_entry ?opaque ?inline ?types ~univs body
+
+let prepare_parameter ~allow_evars ~poly sigma udecl typ =
+  check_definition_evars ~allow_evars sigma;
+  let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
+      sigma (fun nf -> nf typ)
+  in
+  let univs = Evd.check_univ_decl ~poly sigma udecl in
+  sigma, (None(*proof using*), (typ, univs), None(*inline*))
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index b5dacf9ea0..1e3644c371 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -23,3 +23,13 @@ val declare_fix : ?opaque:bool -> definition_kind ->
   Id.t -> Safe_typing.private_constants Entries.proof_output ->
   Constr.types -> Impargs.manual_implicits ->
   GlobRef.t
+
+val prepare_definition : allow_evars:bool ->
+  ?opaque:bool -> ?inline:bool -> poly:bool ->
+  Evd.evar_map -> UState.universe_decl ->
+  types:EConstr.t option -> body:EConstr.t ->
+  Evd.evar_map * Safe_typing.private_constants Entries.definition_entry
+
+val prepare_parameter : allow_evars:bool ->
+  poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types ->
+  Evd.evar_map * Entries.parameter_entry