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.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/vernacinterp.ml')
| -rw-r--r-- | vernac/vernacinterp.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 3e7101834f..70f4fc7b10 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -218,9 +218,9 @@ let interp_qed_delayed ~proof ~pinfo ~st pe : Vernacstate.LemmaStack.t option = let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in let () = match pe with | Admitted -> - Declare.save_lemma_admitted_delayed ~proof ~pinfo + Declare.Proof.save_lemma_admitted_delayed ~proof ~pinfo | Proved (_,idopt) -> - Declare.save_lemma_proved_delayed ~proof ~pinfo ~idopt in + Declare.Proof.save_lemma_proved_delayed ~proof ~pinfo ~idopt in stack let interp_qed_delayed_control ~proof ~pinfo ~st ~control { CAst.loc; v=pe } = |