diff options
Diffstat (limited to 'vernac/declareDef.mli')
| -rw-r--r-- | vernac/declareDef.mli | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 9c5cd6fc2a..8f3db59ba9 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -43,15 +43,17 @@ module ClosedDef : sig type t (* Don't use for non-interactive proofs *) - val of_proof_entry : Evd.side_effects Declare.proof_entry -> t + val of_proof_entry + : uctx:UState.t + -> Evd.side_effects Declare.proof_entry -> t end val declare_definition : name:Id.t -> scope:locality -> kind:Decls.logical_kind - -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list) - -> ubind:UnivNames.universe_binders + -> ?hook:Hook.t + -> ?obls:(Id.t * Constr.t) list -> impargs:Impargs.manual_implicits -> ClosedDef.t -> GlobRef.t @@ -95,9 +97,6 @@ val declare_mutually_recursive -> Recthm.t list -> Names.GlobRef.t list -(* The common use of the returned evar_map is to obtain the universe - binders and context for the hook; we should refactor that soon by - merging prepare and declare. *) val prepare_definition : ?opaque:bool -> ?inline:bool @@ -107,7 +106,7 @@ val prepare_definition -> types:EConstr.t option -> body:EConstr.t -> Evd.evar_map - -> Evd.evar_map * ClosedDef.t + -> ClosedDef.t val prepare_obligation : ?opaque:bool |