By default Coq stdlib warnings raise an error, so this is really required.

Add headers to a few files which were missing them.

This could be Prop (for compat with usual Coq), Set (for HoTT),
 or actually an arbitrary "i".

Take lower bound of universes into account in pretyping/engine

Reinstate proper elaboration of SProp <= l constraints:

replacing is_small with equality with lbound is _not_ semantics preserving!

lbound = Set

Elaborate template polymorphic inductives with lower bound Prop

This will make more constraints explicit

Check univ constraints with Prop as lower bound for template inductives

Restrict template polymorphic universes to those not bounded from below

Fixes #9294

fix suggested by Matthieu

Try second fix suggested by Matthieu

Take care of modifying elaboration for record declarations as well.

Rebase and export functions for debug

Remove exported functions used while debugging

Add a new typing flag "check_template" and option "-no-template-checl"

This parameterizes the new criterion on template polymorphic inductives
to allow bypassing it (necessary for backward compatibility).

Update checker to the new typing flags structure

Switch on the new template_check flag to allow old unsafe behavior in
indTyping.

This is the only change of code really impacting the kernel, together
with the commit implementing unbounded from below and parameterization
by the lower bound on universes.

Add deprecated option `Unset Template Check` allowing to make proof
scripts work with both 8.9 and 8.10 for a while

Fix `Template Check` option name and test it

Add `Unset Template Check` to Coq89.v

Cooking of inductives and template-check tests

Cleanup test-suite file for template check / universes(template) flags

cookind tests

Move test of `Unset Template Check` to the failure/ dir, but comment it
for now

Template test-suite test explanation

Overlays for PR 9918

Overlay for paramcoq

Add overlay for fiat_parsers (-no-template-check)

Add overlay for fiat_crypto_legacy

Update fiat-crypto legacy overlay

Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made.

Remove overlay that should no longer be necessary

The setting in the compat file should handle it

Remove now-merged fiat-crypto-legacy overlay

Update `Print Assumptions` to reflect the typing flag for template checking

Fix About and Print Assumptions for template poly, giving info on which
variables are actually polymorphic

Fix pretty printing to print global universe levels properly

Fix printing of template polymorphic universes

Fix pretty printing for template polymorphism on no universe

Fix interaction of template check and universes(template) flag

Fix indTyping to really check if there is any point in polymorphism: the
conclusion sort should be parameterized over at least one local universe

Indtyping fixes for template polymorphic Props

Allow explicit template polymorphism again

Adapt to new indTyping interface

Handle the case of template-polymorphic on no universes
correctly (morally Type0m univ represented as Prop).

Fix check of meaningfullness of template polymorphism in the kernel.

It is now done w.r.t the min_univ, the minimal universe inferred for the
inductive/record type, independently of the user-written annotation
which must only be larger than min_univ. This preserves compatibility
with UniMath and template-polymorphism as it has been implemented up-to
now.

Comment on identity non-template-polymorphism

Remove incorrect universes(template) attributes from ssr

simpl_fun can be meaningfully template-poly, as well as
pred_key (although the use is debatable: it could just
as well be in Prop).

Move `fun_of_simpl` coercion declaration out of section to respect
uniform inheritance

Remove incorrect uses of #[universes(template)] from the stdlib

Extraction of micromega changes due to moving an ind decl out of a section

Remove incorrect uses of #[universes(template)] from plugins

Fix test-suite files, removing incorrect #[universes(template)] attributes

Remove incorrect #[universes(template)] attributes in test-suite

Fix test-suite

Remove overlays as they have been merged upstream.

ie default goal selector !

How to do this:
- change the default value of default goal selector in goal_select.ml
- eval the emacs code in this commit message
- compile Coq and in each erroring file repeatedly run
  [C-c f] (my/maybe-fix-buller-error) then [C-c C-b] (proof-process-buffer)
  until there are no errors (NB the first [C-c f] has no effect).

You need to watch for 2 cases:
- overly deep proofs where the bullets need to go beyond the list in
  my/bullet-stack (6 layers is enough the vast majority of the time
  though). The system will give you an error and you need to finish
  the lemma manually.

- weird indentation when a bullet starts in the middle of a line and
  doesn't end in that line. Just reindent as you like then go to the
  next error and continue.

~~~emacs-lisp
(defconst my/bullet-stack (list "-" "+" "*" "--" "++" "**")
  "Which bullets should be used, in order.")

(defvar-local my/bullet-count nil
  "The value in the car indicates how many goals remain in the
  bullet at (length-1), and so on recursively. nil means we
  haven't started bulleting the current proof.")

(defvar-local my/last-seen-qed nil)

(defun my/get-maybe-bullet-error ()
  "Extract the number of focused goals from the ! selector error message."
  (when-let* ((rbuf (get-buffer "*response*"))
              (str (with-current-buffer "*response*" (buffer-string)))
              (_ (string-match
                  (rx "Error: Expected a single focused goal but " (group (+ digit)))
                  str))
              (ngoals (string-to-number (match-string 1 str))))
    ngoals))

(defun my/bullet-fix-indent ()
  "Auto indent until the next Qed/Defined, and update my/last-seen-qed."
  ;;  (insert (format "(* %s -> %s *)\n" my/prev-count my/bullet-count))
  (when-let ((qed (save-excursion (search-forward-regexp (rx (or "Defined." "Qed.")) nil t))))
    (set-marker my/last-seen-qed qed)
    (indent-region (- (point) 1) qed)))

(defun my/nth-bullet (n)
  "Get nth bullet, erroring if n >= length my/bullet-stack"
  (or (nth n my/bullet-stack)
      (error "Too many bullets.")))

(defun my/maybe-fix-bullet-error (&optional arg)
  "Main function for porting a file to strict focusing.

Repeatedly process your file in proof general until you get a
focusing error, then run this function. Once there are no more
errors you're done.

Indentation commonly looks bad in the middle of fixing a proof,
but will be fixed unless you start a bullet in the middle of a
line and don't finish it in that line. ie in 'tac1. - tac2.\n
tac3.' tac3 will get indented to align with tac2, but if tac2
finished the bullet the next action will reindent.

This is a stateful process. The state is automatically reset when
you get to the next proof, but if you get an error or take manual
action which breaks the algorithm's expectation you can call with
prefix argument to reset."
  (interactive "P")
  (unless my/last-seen-qed
    (setq my/last-seen-qed (set-marker (make-marker) 0)))
  (when (or arg (> (point) my/last-seen-qed))
    (setq my/bullet-count nil)
    (set-marker my/last-seen-qed 0))

  (when-let ((ngoals (my/get-maybe-bullet-error)))
    (setq my/prev-count (format "%s %s" ngoals my/bullet-count))
    (if (= ngoals 0)
        (progn
          (while (and my/bullet-count (= (car my/bullet-count) 0))
            (pop my/bullet-count))
          (insert (concat (my/nth-bullet (- (length my/bullet-count) 1)) " "))
          (setq my/bullet-count (cons (- (car my/bullet-count) 1) (cdr my/bullet-count)))
          (my/bullet-fix-indent))

      (setq my/bullet-count (cons (- ngoals 1) my/bullet-count))
      (insert (concat (my/nth-bullet (- (length my/bullet-count) 1)) " "))
      (my/bullet-fix-indent))))

(bind-key "C-c f" #'my/maybe-fix-bullet-error coq-mode-map)
~~~

Previously, hints added without a specified database where implicitly
put in the "core" database, which was discouraged by the user manual
(because of the lack of modularity of this approach).