[tactics] Remove dependency of abstract on global proof state.

In order to do so we place the polymorphic status and name in the
read-only part of the monad.

Note the added comments, as well as the fact that almost no part of
tactics depends on `proofs` nor `interp`, thus they should be placed
just after pretyping.

Gaëtan Gilbert noted that ideally, abstract should not depend on the
polymorphic status, should we be able to defer closing of the
constant, however this will require significant effort.

Also, we may deprecate nameless abstract, thus rending both of the
changes this PR need unnecessary.

9 files changed, 9 insertions, 61 deletions

diff --git a/dev/ci/ci-fiat-parsers.sh b/dev/ci/ci-fiat_parsers.sh
index ac74ebf667..ac74ebf667 100755
--- a/dev/ci/ci-fiat-parsers.sh
+++ b/dev/ci/ci-fiat_parsers.sh
diff --git a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh b/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh
deleted file mode 100644
index 6e89741e29..0000000000
--- a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "6914" ] || [ "$CI_BRANCH" = "primitive-bool-list" ]; then
-
-    bignums_CI_REF=primitive-integers
-    bignums_CI_GITURL=https://github.com/vbgl/bignums
-
-    mtac2_CI_REF=primitive-integers
-    mtac2_CI_GITURL=https://github.com/vbgl/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh b/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh
deleted file mode 100644
index 2df8affd14..0000000000
--- a/dev/ci/user-overlays/09102-ejgallego-ltac+remove_aliases.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9102" ] || [ "$CI_BRANCH" = "ltac+remove_aliases" ]; then
-
-    elpi_CI_REF=ltac+remove_aliases
-    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
-
-fi
diff --git a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh b/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh
deleted file mode 100644
index f2a113b118..0000000000
--- a/dev/ci/user-overlays/09150-ejgallego-build+warn_50.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9150" ] || [ "$CI_BRANCH" = "build+warn_50" ]; then
-
-    mtac2_CI_REF=build+warn_50
-    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh b/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh
deleted file mode 100644
index f532fdfc52..0000000000
--- a/dev/ci/user-overlays/09172-ejgallego-proof_rework.sh
+++ /dev/null
@@ -1,9 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9172" ] || [ "$CI_BRANCH" = "proof_rework" ]; then
-
-    ltac2_CI_REF=proof_rework
-    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
-
-    mtac2_CI_REF=proof_rework
-    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
-
-fi
diff --git a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh
new file mode 100644
index 0000000000..23eb24c304
--- /dev/null
+++ b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "9173" ] || [ "$CI_BRANCH" = "proofview+proof_info" ]; then
+
+    ltac2_CI_REF=proofview+proof_info
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+    fiat_parsers_CI_REF=proofview+proof_info
+    fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat
+
+fi
diff --git a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh b/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh
deleted file mode 100644
index efcdd2e97f..0000000000
--- a/dev/ci/user-overlays/09220-maximedenes-stm-shallow-logic.sh
+++ /dev/null
@@ -1,6 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9220" ] || [ "$CI_BRANCH" = "stm-shallow-logic" ]; then
-
-    paramcoq_CI_REF=stm-shallow-logic
-    paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq
-
-fi
diff --git a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh
deleted file mode 100644
index ebd1b524da..0000000000
--- a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9263" ] || [ "$CI_BRANCH" = "parsing-state" ]; then
-
-    mtac2_CI_REF=proof-mode
-    mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2
-
-    ltac2_CI_REF=proof-mode
-    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
-
-    equations_CI_REF=proof-mode
-    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
-
-fi
diff --git a/dev/ci/user-overlays/09410-maximedenes-thread-program.sh b/dev/ci/user-overlays/09410-maximedenes-thread-program.sh
deleted file mode 100644
index 985c2db74e..0000000000
--- a/dev/ci/user-overlays/09410-maximedenes-thread-program.sh
+++ /dev/null
@@ -1,13 +0,0 @@
-if [ "$CI_PULL_REQUEST" = "9410" ] || [ "$CI_BRANCH" = "thread-program" ]; then
-
-    math_classes_CI_REF=program-mode-flag
-    math_classes_CI_GITURL=https://github.com/maximedenes/math-classes
-
-    ltac2_CI_REF=program-mode-flag
-    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
-
-
-    equations_CI_REF=thread-program
-    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
-
-fi