From c27e98f61216d08cb999c3b60067defacb15e104 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 24 Oct 2023 14:26:57 +0200
Subject: [PATCH] Fix Vernactypes.vtnoproof to actually reject open proofs

In practice this only changes Register as there are no other users and it's
not exposed by coqpp, unless some plugin calls it directly.
---
 vernac/vernactypes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vernac/vernactypes.ml b/vernac/vernactypes.ml
index fc9580b4a39a..27780cdb83f6 100644
--- a/vernac/vernactypes.ml
+++ b/vernac/vernactypes.ml
@@ -83,7 +83,7 @@ let vtdefault f =
                     (), ()) }
 
 let vtnoproof f =
-  TypedVernac { inprog = Ignore; outprog = No; inproof = Ignore; outproof = No;
+  TypedVernac { inprog = Ignore; outprog = No; inproof = Reject; outproof = No;
                 run = (fun ~pm:() ~proof:() ->
                     let () = f () in
                     (), ())