diff options
| -rw-r--r-- | plugins/ltac/g_obligations.mlg | 8 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_13755.v | 5 | ||||
| -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 |
6 files changed, 17 insertions, 10 deletions
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 6bf330c830..e7902d06eb 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -151,13 +151,13 @@ VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY END VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY STATE read_program -| [ "Obligations" "of" ident(name) ] -> { show_obligations (Some name) } -| [ "Obligations" ] -> { show_obligations None } +| [ "Obligations" "of" ident(name) ] -> { fun ~stack:_ -> show_obligations (Some name) } +| [ "Obligations" ] -> { fun ~stack:_ -> show_obligations None } END VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY STATE read_program -| [ "Preterm" "of" ident(name) ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) } -| [ "Preterm" ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm None) } +| [ "Preterm" "of" ident(name) ] -> { fun ~stack:_ ~pm -> Feedback.msg_notice (show_term ~pm (Some name)) } +| [ "Preterm" ] -> { fun ~stack:_ ~pm -> Feedback.msg_notice (show_term ~pm None) } END { diff --git a/test-suite/bugs/closed/bug_13755.v b/test-suite/bugs/closed/bug_13755.v new file mode 100644 index 0000000000..cc25157b9b --- /dev/null +++ b/test-suite/bugs/closed/bug_13755.v @@ -0,0 +1,5 @@ +Module M1. +Lemma t1 : True. +Fail End M1. +Proof. exact I. Qed. +End M1. 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 -> |