diff options
Diffstat (limited to 'vernac/lemmas.mli')
| -rw-r--r-- | vernac/lemmas.mli | 15 |
1 files changed, 1 insertions, 14 deletions
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 471c955311..6a1f8c09f3 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -44,19 +44,6 @@ module Proof_ending : sig end -module Recthm : sig - type t = - { name : Id.t - (** Name of theorem *) - ; typ : Constr.t - (** Type of theorem *) - ; args : Name.t list - (** Names to pre-introduce *) - ; impargs : Impargs.manual_implicits - (** Explicitily declared implicit arguments *) - } -end - module Info : sig type t @@ -104,7 +91,7 @@ val start_lemma_with_initialization -> udecl:UState.universe_decl -> Evd.evar_map -> (bool * lemma_possible_guards * Constr.t option list option) option - -> Recthm.t list + -> DeclareDef.Recthm.t list -> int list option -> t |