diff options
Diffstat (limited to 'vernac/comFixpoint.mli')
| -rw-r--r-- | vernac/comFixpoint.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 62a9d10bae..486d0156f9 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -16,13 +16,13 @@ open Vernacexpr (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint_interactive : - scope:Declare.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t + scope:Declare.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t val do_fixpoint : scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit val do_cofixpoint_interactive : - scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t + scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t val do_cofixpoint : scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit |