13 files changed, 90 insertions, 5 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index a6ed9be58d..f6c035553c 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -693,6 +693,9 @@ library:ci-color:
 library:ci-compcert:
   extends: .ci-template-flambda
 
+library:ci-coq_performance_tests:
+  extends: .ci-template
+
 library:ci-coq_tools:
   extends: .ci-template
 
diff --git a/Makefile.ci b/Makefile.ci
index 9231fa6fed..07f06caa3a 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -20,6 +20,7 @@ CI_TARGETS= \
     ci-coquelicot \
     ci-corn \
     ci-cross_crypto \
+    ci-coq_performance_tests \
     ci-coq_tools \
     ci-coqprime \
     ci-elpi \
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 475f812b5a..88471a92aa 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -95,6 +95,13 @@
 : "${flocq_CI_ARCHIVEURL:=${flocq_CI_GITURL}/-/archive}"
 
 ########################################################################
+# coq-performance-tests
+########################################################################
+: "${coq_performance_tests_CI_REF:=master}"
+: "${coq_performance_tests_CI_GITURL:=https://github.com/coq-community/coq-performance-tests}"
+: "${coq_performance_tests_CI_ARCHIVEURL:=${coq_performance_tests_CI_GITURL}/archive}"
+
+########################################################################
 # coq-tools
 ########################################################################
 : "${coq_tools_CI_REF:=master}"
diff --git a/dev/ci/ci-coq_performance_tests.sh b/dev/ci/ci-coq_performance_tests.sh
new file mode 100755
index 0000000000..4eb77cfb24
--- /dev/null
+++ b/dev/ci/ci-coq_performance_tests.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download coq_performance_tests
+
+( cd "${CI_BUILD_DIR}/coq_performance_tests" && make coq perf && make validate && make install )
diff --git a/doc/changelog/04-tactics/12552-zify-pre-hook.rst b/doc/changelog/04-tactics/12552-zify-pre-hook.rst
new file mode 100644
index 0000000000..975c917b19
--- /dev/null
+++ b/doc/changelog/04-tactics/12552-zify-pre-hook.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Thhe :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook`
+  tactic. (`#12552 <https://github.com/coq/coq/pull/12552>`_,
+  by Kazuhiko Sakaguchi).
diff --git a/doc/changelog/09-coqide/12562-coqide-lax-filename.rst b/doc/changelog/09-coqide/12562-coqide-lax-filename.rst
new file mode 100644
index 0000000000..ef3160dd99
--- /dev/null
+++ b/doc/changelog/09-coqide/12562-coqide-lax-filename.rst
@@ -0,0 +1,4 @@
+- **Fixed:** CoqIDE no longer exits when trying to open a file whose name is not a valid identifier
+  (`#12562 <https://github.com/coq/coq/pull/12562>`_,
+  fixes `#10988 <https://github.com/coq/coq/issues/10988>`_,
+  by Vincent Laporte).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index c4947e6b3a..c01e6a5aa6 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -278,7 +278,8 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
 
    This tactic is internally called by :tacn:`lia` to support additional types e.g., :g:`nat`, :g:`positive` and :g:`N`.
    By requiring the module ``ZifyBool``, the boolean type :g:`bool` and some comparison operators are also supported.
-   :tacn:`zify` can also be extended by rebinding the tactic `Zify.zify_post_hook` that is run immediately after :tacn:`zify`.
+   :tacn:`zify` can also be extended by rebinding the tactics `Zify.zify_pre_hook` and `Zify.zify_post_hook` that are
+   respectively run in the first and the last steps of :tacn:`zify`.
 
    + To support :g:`Z.div` and :g:`Z.modulo`: ``Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations``.
    + To support :g:`Z.quot` and :g:`Z.rem`: ``Ltac Zify.zify_post_hook ::= Z.quot_rem_to_equations``.
diff --git a/ide/coqide/coqide.ml b/ide/coqide/coqide.ml
index ab2a17798e..b66da11e7b 100644
--- a/ide/coqide/coqide.ml
+++ b/ide/coqide/coqide.ml
@@ -114,8 +114,10 @@ let make_coqtop_args fname =
         (* We basically copy the code of Names.check_valid since it is not exported *)
         (* to coqide. This is to prevent a possible failure of parsing  "-topfile"  *)
         (* at initialization of coqtop (see #10286) *)
+        (* If the file name is a valid identifier, use it as toplevel name; *)
+        (* otherwise the default “Top” will be used. *)
         match Unicode.ident_refutation (Filename.chop_extension (Filename.basename fname)) with
-        | Some (_,x) -> output_string stderr (x^"\n"); exit 1
+        | Some _ -> args
         | None -> "-topfile"::fname::args
   in
   proj, args
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index cb868e0480..342175a512 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -55,7 +55,7 @@ exception ComplexSort
 
 let glob_sort_family = let open Sorts in function
   | UAnonymous {rigid=true} -> InType
-  | UNamed [GSProp,0] -> InProp
+  | UNamed [GSProp,0] -> InSProp
   | UNamed [GProp,0] -> InProp
   | UNamed [GSet,0] -> InSet
   | _ -> raise ComplexSort
diff --git a/test-suite/bugs/closed/bug_12529.v b/test-suite/bugs/closed/bug_12529.v
new file mode 100644
index 0000000000..bc3c9a28bd
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12529.v
@@ -0,0 +1,21 @@
+Goal SProp.
+match goal with |- SProp => idtac end.
+Fail match goal with |- Prop => idtac end.
+Abort.
+
+Goal Prop.
+Fail match goal with |- SProp => idtac end.
+match goal with |- Prop => idtac end.
+Abort.
+
+Class F A := f : A.
+
+Inductive pFalse : Prop  := .
+Inductive sFalse : SProp := .
+
+Hint Extern 0 (F Prop) => exact pFalse : typeclass_instances.
+Definition pf := f : Prop.
+
+Hint Extern 0 (F SProp) => exact sFalse : typeclass_instances.
+Definition sf := (f : SProp).
+Definition pf' := (f : Prop).
diff --git a/test-suite/micromega/zify.v b/test-suite/micromega/zify.v
index 8fd7398638..a12623c3c0 100644
--- a/test-suite/micromega/zify.v
+++ b/test-suite/micromega/zify.v
@@ -159,7 +159,7 @@ Require Import ZifyClasses.
 Require Import ZifyInst.
 
 Instance Zero : CstOp (@zero znat : nat) := Op_O.
-Add CstOp Zero.
+Add Zify CstOp Zero.
 
 
 Goal  @zero znat = 0%nat.
@@ -227,3 +227,12 @@ Goal forall (f : Z -> bool), negb (negb (f 0)) = f 0.
 Proof.
   intros. lia.
 Qed.
+
+Ltac Zify.zify_pre_hook ::= unfold is_true in *.
+
+Goal forall x y : nat, is_true (Nat.eqb x 1) ->
+                       is_true (Nat.eqb y 0) ->
+                       is_true (Nat.eqb (x + y) 1).
+Proof.
+lia.
+Qed.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 33e40a115b..4fa8b3216a 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1774,6 +1774,28 @@ Proof.
   now rewrite <- INR_IPR, SuccNat2Pos.id_succ.
 Qed.
 
+Lemma IZR_NEG : forall p, IZR (Zneg p) = Ropp (IZR (Zpos p)).
+Proof.
+  reflexivity.
+Qed.
+
+(** The three following lemmas map the default form of numerical
+    constants to their representation in terms of the axioms of
+    [R]. This can be a useful intermediate representation for reifying
+    to another axiomatics of the reals. It is however generally more
+    convenient to keep constants represented under an [IZR z] form when
+    working within [R]. *)
+
+Lemma IZR_POS_xO : forall p, IZR (Zpos (xO p)) = (1+1) * (IZR (Zpos p)).
+Proof.
+  intro. unfold IZR, IPR. destruct p; simpl; trivial. rewrite Rmult_1_r. trivial.
+Qed.
+
+Lemma IZR_POS_xI : forall p, IZR (Zpos (xI p)) = 1 + (1+1) * IZR (Zpos p).
+Proof.
+  intro. unfold IZR, IPR. destruct p; simpl; trivial. rewrite Rmult_1_r. trivial.
+Qed.
+
 Lemma plus_IZR_NEG_POS :
   forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q).
 Proof.
diff --git a/theories/micromega/Zify.v b/theories/micromega/Zify.v
index 2df3c57d32..183fd6a914 100644
--- a/theories/micromega/Zify.v
+++ b/theories/micromega/Zify.v
@@ -11,12 +11,15 @@
 Require Import ZifyClasses ZifyInst.
 Declare ML Module "zify_plugin".
 
-(** [zify_post_hook] is there to be redefined. *)
+(** [zify_pre_hook] and [zify_post_hook] are there to be redefined. *)
+Ltac zify_pre_hook := idtac.
+
 Ltac zify_post_hook := idtac.
 
 Ltac iter_specs := zify_iter_specs.
 
 Ltac zify := intros;
+             zify_pre_hook ;
              zify_elim_let ;
              zify_op ;
              (zify_iter_specs) ;