From 6e41dd8c6ba0279b9c882c02053c4d34eb251971 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 26 Jan 2021 12:10:11 +0100
Subject: [vernac] Check that no proofs do remain open at section/module
 closing time

Fixes #13755 .
---
 vernac/vernacentries.ml | 8 +++++---
 vernac/vernacextend.ml  | 2 +-
 vernac/vernacextend.mli | 2 +-
 vernac/vernacinterp.ml  | 2 +-
 4 files changed, 8 insertions(+), 6 deletions(-)

(limited to 'vernac')

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 ->
-- 
cgit v1.2.3