diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-13 01:06:48 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-13 17:48:48 +0100 |
| commit | c75619228e1c878644edbc49c5cb690777966863 (patch) | |
| tree | b02c141f35893656559548f688873abb286db4dd /vernac/lemmas.mli | |
| parent | b0f716e7c23f3095cf0cd96c79d762835ebdff23 (diff) | |
[econstr] Small cleanup in `vernac/lemmas`
Diffstat (limited to 'vernac/lemmas.mli')
| -rw-r--r-- | vernac/lemmas.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index a4854b4a6..ca92e856b 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Constr open Decl_kinds type 'a declaration_hook @@ -37,11 +36,11 @@ val start_proof_com : goal_kind -> Vernacexpr.proof_expr list -> unit declaration_hook -> unit -val start_proof_with_initialization : +val start_proof_with_initialization : goal_kind -> Evd.evar_map -> Univdecls.universe_decl -> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option -> (Id.t (* name of thm *) * - (types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list + (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit val universe_proof_terminator : |