From e7d1d0461c51de9ae955bd0ce2a0d977cf7a437a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 5 Dec 2018 13:35:27 +0100
Subject: High level functions to produce kernel entries from econstr.

---
 vernac/declareDef.mli | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'vernac/declareDef.mli')

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