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/vernacstate.ml | |
| 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/vernacstate.ml')
| -rw-r--r-- | vernac/vernacstate.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index cb45dc9e15..17c89897fe 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -152,17 +152,17 @@ module Declare = struct s_lemmas := Some stack; res - type closed_proof = Declare.proof_object * Declare.Proof.Proof_info.t + type closed_proof = Declare.Proof.proof_object * Declare.Proof.Proof_info.t - let return_proof () = cc Declare.return_proof - let return_partial_proof () = cc Declare.return_partial_proof + let return_proof () = cc Declare.Proof.return_proof + let return_partial_proof () = cc Declare.Proof.return_partial_proof let close_future_proof ~feedback_id pf = - cc (fun pt -> Declare.close_future_proof ~feedback_id pt pf, + cc (fun pt -> Declare.Proof.close_future_proof ~feedback_id pt pf, Declare.Proof.info pt) let close_proof ~opaque ~keep_body_ucst_separate = - cc (fun pt -> Declare.close_proof ~opaque ~keep_body_ucst_separate pt, + cc (fun pt -> Declare.Proof.close_proof ~opaque ~keep_body_ucst_separate pt, Declare.Proof.info pt) let discard_all () = s_lemmas := None |