diff options
Diffstat (limited to 'vernac/vernacextend.ml')
| -rw-r--r-- | vernac/vernacextend.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index d772f274a2..f8a80e8feb 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -55,8 +55,8 @@ and proof_block_name = string (** open type of delimiters *) type typed_vernac = | VtDefault of (unit -> unit) | VtNoProof of (unit -> unit) - | VtCloseProof of (lemma:Lemmas.t -> unit) - | VtOpenProof of (unit -> Lemmas.t) + | VtCloseProof of (lemma:Declare.Proof.t -> unit) + | VtOpenProof of (unit -> Declare.Proof.t) | VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t) | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit) | VtReadProof of (pstate:Declare.Proof.t -> unit) |