diff options
| author | Emilio Jesus Gallego Arias | 2020-11-20 02:44:53 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-11-20 02:44:53 +0100 |
| commit | b832d484f7cf8e32cd231a079a6336f2b1b0bad4 (patch) | |
| tree | 86649c5e305a5cbea7d3629bc987dfbdb8d9fdfe /vernac/vernacinterp.ml | |
| parent | 36aeb43062aa6671020457538577311fbe7d7b3a (diff) | |
[stm] [declare] Remove pinfo internals hack.
After the previous commit, the stm should correctly pass proof
information, thus we make `proof_object` carry it removing a bunch of
internal code.
Diffstat (limited to 'vernac/vernacinterp.ml')
| -rw-r--r-- | vernac/vernacinterp.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index edf48fef1a..57d9e0ac3c 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -226,24 +226,24 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) = *) (* Interpreting a possibly delayed proof *) -let interp_qed_delayed ~proof ~pinfo ~st pe : Vernacstate.LemmaStack.t option * Declare.OblState.t = +let interp_qed_delayed ~proof ~st pe : Vernacstate.LemmaStack.t option * Declare.OblState.t = let stack = st.Vernacstate.lemmas in let pm = st.Vernacstate.program in let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in let pm = match pe with | Admitted -> - Declare.Proof.save_lemma_admitted_delayed ~pm ~proof ~pinfo + Declare.Proof.save_lemma_admitted_delayed ~pm ~proof | Proved (_,idopt) -> - let pm, _ = Declare.Proof.save_lemma_proved_delayed ~pm ~proof ~pinfo ~idopt in + let pm, _ = Declare.Proof.save_lemma_proved_delayed ~pm ~proof ~idopt in pm in stack, pm -let interp_qed_delayed_control ~proof ~pinfo ~st ~control { CAst.loc; v=pe } = +let interp_qed_delayed_control ~proof ~st ~control { CAst.loc; v=pe } = let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn) control - (fun ~st -> interp_qed_delayed ~proof ~pinfo ~st pe) + (fun ~st -> interp_qed_delayed ~proof ~st pe) ~st (* General interp with management of state *) @@ -273,6 +273,6 @@ let interp_gen ~verbosely ~st ~interp_fn cmd = let interp ?(verbosely=true) ~st cmd = interp_gen ~verbosely ~st ~interp_fn:interp_control cmd -let interp_qed_delayed_proof ~proof ~pinfo ~st ~control pe : Vernacstate.t = +let interp_qed_delayed_proof ~proof ~st ~control pe : Vernacstate.t = interp_gen ~verbosely:false ~st - ~interp_fn:(interp_qed_delayed_control ~proof ~pinfo ~control) pe + ~interp_fn:(interp_qed_delayed_control ~proof ~control) pe |