diff options
| author | Emilio Jesus Gallego Arias | 2020-06-23 21:48:23 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:12 +0200 |
| commit | bf31fad28992a67b66d859655f030e619b69705e (patch) | |
| tree | 878e41ee13f2891edf19ed6ad25b29ed11f03264 /vernac/vernacinterp.mli | |
| parent | ea8b9e060dfba9cc8706677e29c26dabaaa87551 (diff) | |
[declare] Improve logical code order
Now that the interface has mostly stabilized, we move code around to
respect internal dependency order.
This will allow us to start sharing more code in the 4 principal
cases, and also paves the way for the full merging of obligations and
the removal of the Proof_ending type in favor of stronger type
abstraction.
Diffstat (limited to 'vernac/vernacinterp.mli')
| -rw-r--r-- | vernac/vernacinterp.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index 35ae4f2296..84d3256c9f 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -14,7 +14,7 @@ val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> (** Execute a Qed but with a proof_object which may contain a delayed proof and won't be forced *) val interp_qed_delayed_proof - : proof:Declare.proof_object + : proof:Declare.Proof.proof_object -> pinfo:Declare.Proof.Proof_info.t -> st:Vernacstate.t -> control:Vernacexpr.control_flag list |