Allow Program to be used with noinit

[Alizter]

Currently Program cannot be used without loading the Coq standard library. Writing something like this with -noinit demonstrates the issue:

Program Definition test : Type := Type.
(** 
Errors:
Library Coq.Init.Datatypes has to be required first.;
*)

by adding:

From Coq Require Import Init.
From Coq Require Import Program.

this is fixed.

I would like to request the ability to register the constants used by Program internally so that we can use it without loading the Coq standard library.

[SkySkimmer]

Should work since 6847eb22a54fd2896677f233b972008a24bf5fdc (https://github.com/coq/coq/pull/18350, 8.20)

[Alizter]

@SkySkimmer Looking at the code, I still see this:

https://github.com/coq/coq/blob/c67f36dc0d7954383cd9a6a03317ff0fd49aa590/vernac/declare.ml#L2719-L2721

[SkySkimmer]

Removing the check seems to work, but the Next Obligation syntax needs ltac plugin. Not sure if that means we should just remove the check (noinit users can figure out how to fix such syntax errors).

[Alizter]

I think requiring the ltac plugin is fine. In the future if ltac2 is to be separated completely from ltac1 then it might make sense to consider something else here to get standalone ltac2 and program working. Just requiring the ltac plugin is a net improvement over the current situation.