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

@@ -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
                     (), ())