diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 8 | ||||
| -rw-r--r-- | vernac/vernacextend.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacextend.mli | 2 | ||||
| -rw-r--r-- | vernac/vernacinterp.ml | 2 |
4 files changed, 8 insertions, 6 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 1c774a35bf..481bc3071b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1215,9 +1215,11 @@ let msg_of_subsection ss id = in Pp.str kind ++ spc () ++ Id.print id -let vernac_end_segment ~pm ({v=id} as lid) = +let vernac_end_segment ~pm ~stack ({v=id} as lid) = let ss = Lib.find_opening_node id in let what_for = msg_of_subsection ss lid.v in + if Option.has_some stack then + CErrors.user_err (Pp.str "Command not supported (Open proofs remain)"); Declare.Obls.check_solved_obligations ~pm ~what_for; match ss with | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid @@ -2173,9 +2175,9 @@ let translate_vernac ~atts v = let open Vernacextend in match v with VtNoProof(fun () -> vernac_begin_section ~poly:(only_polymorphism atts) lid) | VernacEndSegment lid -> - VtReadProgram(fun ~pm -> + VtReadProgram(fun ~stack ~pm -> unsupported_attributes atts; - vernac_end_segment ~pm lid) + vernac_end_segment ~pm ~stack lid) | VernacNameSectionHypSet (lid, set) -> VtDefault(fun () -> unsupported_attributes atts; diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index ed63332861..f320b65954 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -59,7 +59,7 @@ type typed_vernac = | VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t) | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit) | VtReadProof of (pstate:Declare.Proof.t -> unit) - | VtReadProgram of (pm:Declare.OblState.t -> unit) + | VtReadProgram of (stack:Vernacstate.LemmaStack.t option -> pm:Declare.OblState.t -> unit) | VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t) | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t) | VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t) diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index e1e3b4cfe5..070c737882 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -77,7 +77,7 @@ type typed_vernac = | VtModifyProof of (pstate:Declare.Proof.t -> Declare.Proof.t) | VtReadProofOpt of (pstate:Declare.Proof.t option -> unit) | VtReadProof of (pstate:Declare.Proof.t -> unit) - | VtReadProgram of (pm:Declare.OblState.t -> unit) + | VtReadProgram of (stack:Vernacstate.LemmaStack.t option -> pm:Declare.OblState.t -> unit) | VtModifyProgram of (pm:Declare.OblState.t -> Declare.OblState.t) | VtDeclareProgram of (pm:Declare.OblState.t -> Declare.Proof.t) | VtOpenProofProgram of (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t) diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 3a8a80d25a..e42775b76c 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -48,7 +48,7 @@ let interp_typed_vernac c ~pm ~stack = vernac_require_open_lemma ~stack (Vernacstate.LemmaStack.with_top ~f:(fun pstate -> f ~pstate)); stack, pm - | VtReadProgram f -> f ~pm; stack, pm + | VtReadProgram f -> f ~stack ~pm; stack, pm | VtModifyProgram f -> let pm = f ~pm in stack, pm | VtDeclareProgram f -> |