diff options
Diffstat (limited to 'vernac/declare.mli')
| -rw-r--r-- | vernac/declare.mli | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/vernac/declare.mli b/vernac/declare.mli index ef4f8c4825..979bdd4334 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -305,13 +305,11 @@ val declare_definition -> ?inline:bool -> types:EConstr.t option -> body:EConstr.t - -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> Evd.evar_map -> GlobRef.t val declare_assumption - : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) - -> name:Id.t + : name:Id.t -> scope:locality -> hook:Hook.t option -> impargs:Impargs.manual_implicits @@ -495,11 +493,6 @@ val obl_substitution : val dependencies : Obligation.t array -> int -> Int.Set.t -(* This is a hack to make it possible for Obligations to craft a Qed - * behind the scenes. The fix_exn the Stm attaches to the Future proof - * is not available here, so we provide a side channel to get it *) -val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) ref - end (** Creating high-level proofs with an associated constant *) |