diff options
| author | Emilio Jesus Gallego Arias | 2020-03-14 16:34:30 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 19:05:37 -0400 |
| commit | 8fbc927ac40cc707b1a940d8339a2a289755d533 (patch) | |
| tree | 878bc7f245ca49f8049d67576f7311de7f37716d /vernac/declareDef.mli | |
| parent | dc03a4d9a7b527df0c2e571de55fd200666bdb11 (diff) | |
[declareDef] More consistent handling of universe binders
The only reasons that `prepare_definition` returned a sigma were:
- to obtain the universe binders to be passed to declare
- to obtain the UState.t to be passed to the equations hook
We handle this automatically now; it seems like a reasonably good API
improvement.
However, it is not clear what we do now is right for all cases; must
check.
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 |