21 files changed, 221 insertions, 124 deletions

diff --git a/.gitignore b/.gitignore
index bf7430cc2e..1abead3c67 100644
--- a/.gitignore
+++ b/.gitignore
@@ -115,6 +115,9 @@ doc/stdlib/index-body.html
 doc/stdlib/index-list.html
 doc/tools/docgram/editedGrammar
 doc/tools/docgram/prodnGrammar
+doc/tools/docgram/prodnCommands
+doc/tools/docgram/prodnTactics
+doc/tools/docgram/updated_rsts
 doc/unreleased.rst
 
 # .mll files
diff --git a/clib/cThread.ml b/clib/cThread.ml
index 89ca2f7d83..3796fdf788 100644
--- a/clib/cThread.ml
+++ b/clib/cThread.ml
@@ -107,3 +107,22 @@ let mask_sigalrm f x =
 
 let create f x =
   Thread.create (mask_sigalrm f) x
+
+(*
+  Atomic mutex lock taken from https://gitlab.com/gadmm/memprof-limits/-/blob/master/src/thread_map.ml#L23-34
+  Critical sections :
+   - Mutex.lock does not poll on leaving the blocking section
+     since 4.12.
+   - Never inline, to avoid theoretically-possible reorderings with
+     flambda.
+     (workaround to the lack of masking)
+*)
+
+(* We inline the call to Mutex.unlock to avoid polling in bytecode mode *)
+external unlock: Mutex.t -> unit = "caml_mutex_unlock"
+
+let[@inline never] with_lock m ~scope =
+  let () = Mutex.lock m (* BEGIN ATOMIC *) in
+  match (* END ATOMIC *) scope () with
+  | (* BEGIN ATOMIC *) x -> unlock m ; (* END ATOMIC *) x
+  | (* BEGIN ATOMIC *) exception e -> unlock m ; (* END ATOMIC *) raise e
diff --git a/clib/cThread.mli b/clib/cThread.mli
index 87889f3356..d974135d43 100644
--- a/clib/cThread.mli
+++ b/clib/cThread.mli
@@ -29,3 +29,8 @@ val thread_friendly_really_read_line : thread_ic -> string
 (* Wrapper around Thread.create that blocks signals such as Sys.sigalrm (used
  * for Timeout *)
 val create : ('a -> 'b) -> 'a -> Thread.t
+
+(*
+  Atomic mutex lock taken from https://gitlab.com/gadmm/memprof-limits/-/blob/master/src/thread_map.ml#L23-34
+*)
+val with_lock : Mutex.t -> scope:(unit -> 'a) -> 'a
diff --git a/clib/exninfo.ml b/clib/exninfo.ml
index 07b7f47529..4c1f47df30 100644
--- a/clib/exninfo.ml
+++ b/clib/exninfo.ml
@@ -71,10 +71,9 @@ let record_backtrace b =
 let get_backtrace e = get e backtrace_info
 
 let iraise (e,i) =
-  let () = Mutex.lock lock in
-  let id = Thread.id (Thread.self ()) in
-  let () = current := (id, (e,i)) :: remove_assoc id !current in
-  let () = Mutex.unlock lock in
+  CThread.with_lock lock ~scope:(fun () ->
+      let id = Thread.id (Thread.self ()) in
+      current := (id, (e,i)) :: remove_assoc id !current);
   match get i backtrace_info with
   | None ->
     raise e
@@ -82,12 +81,11 @@ let iraise (e,i) =
     Printexc.raise_with_backtrace e bt
 
 let find_and_remove () =
-  let () = Mutex.lock lock in
-  let id = Thread.id (Thread.self ()) in
-  let (v, l) = find_and_remove_assoc id !current in
-  let () = current := l in
-  let () = Mutex.unlock lock in
-  v
+  CThread.with_lock lock ~scope:(fun () ->
+      let id = Thread.id (Thread.self ()) in
+      let (v, l) = find_and_remove_assoc id !current in
+      let () = current := l in
+      v)
 
 let info e =
   let (src, data) = find_and_remove () in
diff --git a/doc/sphinx/_static/ansi.css b/doc/sphinx/_static/ansi.css
index 2a618f68d2..a4850a738b 100644
--- a/doc/sphinx/_static/ansi.css
+++ b/doc/sphinx/_static/ansi.css
@@ -69,7 +69,7 @@
 }
 
 .ansi-fg-white {
-    color: #2e3436;
+    color: #ffffff;
 }
 
 .ansi-fg-light-black {
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 9f097b4fe9..abe928fa26 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -5,7 +5,7 @@ The underlying formal language of Coq is a
 :gdef:`Calculus of Inductive Constructions` (|Cic|) whose inference rules
 are presented in this
 chapter. The history of this formalism as well as pointers to related
-work are provided in a separate chapter; see *Credits*.
+work are provided in a separate chapter; see :ref:`history`.
 
 
 .. _The-terms:
diff --git a/doc/tools/coqrst/repl/ansicolors.py b/doc/tools/coqrst/repl/ansicolors.py
index 9e23be2409..6700c20b1a 100644
--- a/doc/tools/coqrst/repl/ansicolors.py
+++ b/doc/tools/coqrst/repl/ansicolors.py
@@ -91,7 +91,10 @@ def parse_ansi(code):
                  leading ‘^[[’ or the final ‘m’
     """
     classes = []
-    parse_style([int(c) for c in code.split(';')], 0, classes)
+    if code == "37":
+        pass # ignore white fg
+    else:
+        parse_style([int(c) for c in code.split(';')], 0, classes)
     return ["ansi-" + cls for cls in classes]
 
 if __name__ == '__main__':
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index ab1a9d4c75..0c8980b1bd 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1778,7 +1778,6 @@ simple_tactic: [
 | "zify_iter_let" tactic      (* micromega plugin *)
 | "zify_elim_let"      (* micromega plugin *)
 | "nsatz_compute" constr      (* nsatz plugin *)
-| "omega"      (* omega plugin *)
 | "protect_fv" string "in" ident      (* ring plugin *)
 | "protect_fv" string      (* ring plugin *)
 | "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr      (* ring plugin *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 5b19b7fc55..40bb980e90 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1856,7 +1856,6 @@ simple_tactic: [
 | "zify_iter_let" ltac_expr      (* micromega plugin *)
 | "zify_elim_let"      (* micromega plugin *)
 | "nsatz_compute" one_term      (* nsatz plugin *)
-| "omega"      (* omega plugin *)
 | "protect_fv" string OPT ( "in" ident )
 | "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term      (* ring plugin *)
 | "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term      (* ring plugin *)
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index 72b54d329f..0a0b932c46 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -489,11 +489,11 @@ let eval_call c =
 let print_xml =
   let m = Mutex.create () in
   fun oc xml ->
-    Mutex.lock m;
-    if !Flags.xml_debug then
-      Printf.printf "SENT --> %s\n%!" (Xml_printer.to_string_fmt xml);
-    try Control.protect_sigalrm (Xml_printer.print oc) xml; Mutex.unlock m
-    with e -> let e = Exninfo.capture e in Mutex.unlock m; Exninfo.iraise e
+    CThread.with_lock m ~scope:(fun () ->
+        if !Flags.xml_debug then
+          Printf.printf "SENT --> %s\n%!" (Xml_printer.to_string_fmt xml);
+        try Control.protect_sigalrm (Xml_printer.print oc) xml
+        with e -> let e = Exninfo.capture e in Exninfo.iraise e)
 
 let slave_feeder fmt xml_oc msg =
   let xml = Xmlprotocol.(of_feedback fmt msg) in
diff --git a/lib/future.ml b/lib/future.ml
index 23d089fb6b..247b139798 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -112,8 +112,8 @@ let create_delegate ?(blocking=true) ~name fix_exn =
     if not blocking then (fun () -> raise (NotReady name)), ignore else
     let lock = Mutex.create () in
     let cond = Condition.create () in
-    (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock),
-    (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in
+    (fun () -> CThread.with_lock lock ~scope:(fun () -> Condition.wait cond lock)),
+    (fun () -> CThread.with_lock lock ~scope:(fun () -> Condition.broadcast cond)) in
   let ck = create ~name ~fix_exn (Delegated wait) in
   ck, assignment signal ck
 
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index 5e1150146e..9ea751eef9 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -28,10 +28,10 @@ let new_counter ~name a ~incr ~build =
          managers (that are threads) and the main thread, hence the mutex *)
     if Flags.async_proofs_is_worker () then
       CErrors.anomaly(Pp.str"Slave processes must install remote counters.");
-    Mutex.lock m; let x = f () in Mutex.unlock m;
+    let x = CThread.with_lock m ~scope:f in
     build x in
   let mk_thsafe_remote_getter f () =
-    Mutex.lock m; let x = f () in Mutex.unlock m; x in
+    CThread.with_lock m ~scope:f in
   let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in
   let installer f =
     if not (Flags.async_proofs_is_worker ()) then
diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg
index 74b0708743..d18065088c 100644
--- a/plugins/micromega/g_zify.mlg
+++ b/plugins/micromega/g_zify.mlg
@@ -24,17 +24,17 @@ let warn_deprecated_Spec =
 DECLARE PLUGIN "zify_plugin"
 
 VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF
-| ["Add" "Zify" "InjTyp"    constr(t) ] -> { Zify.InjTable.register t }
-| ["Add" "Zify" "BinOp"     constr(t) ] -> { Zify.BinOp.register t }
-| ["Add" "Zify" "UnOp"      constr(t) ] -> { Zify.UnOp.register t }
-| ["Add" "Zify" "CstOp"     constr(t) ] -> { Zify.CstOp.register t }
-| ["Add" "Zify" "BinRel"    constr(t) ] -> { Zify.BinRel.register t }
-| ["Add" "Zify" "PropOp"    constr(t) ] -> { Zify.PropBinOp.register t }
-| ["Add" "Zify" "PropBinOp"    constr(t) ] -> { Zify.PropBinOp.register t }
-| ["Add" "Zify" "PropUOp"   constr(t) ] -> { Zify.PropUnOp.register t }
-| ["Add" "Zify" "BinOpSpec" constr(t) ] -> { Zify.BinOpSpec.register t }
-| ["Add" "Zify" "UnOpSpec"  constr(t) ] -> { Zify.UnOpSpec.register t }
-| ["Add" "Zify" "Saturate"  constr(t) ] -> { Zify.Saturate.register t }
+| ["Add" "Zify" "InjTyp"   reference(t) ] -> { Zify.InjTable.register t }
+| ["Add" "Zify" "BinOp"     reference(t) ] -> { Zify.BinOp.register t }
+| ["Add" "Zify" "UnOp"      reference(t) ] -> { Zify.UnOp.register t }
+| ["Add" "Zify" "CstOp"     reference(t) ] -> { Zify.CstOp.register t }
+| ["Add" "Zify" "BinRel"    reference(t) ] -> { Zify.BinRel.register t }
+| ["Add" "Zify" "PropOp"    reference(t) ] -> { Zify.PropBinOp.register t }
+| ["Add" "Zify" "PropBinOp"    reference(t) ] -> { Zify.PropBinOp.register t }
+| ["Add" "Zify" "PropUOp"   reference(t) ] -> { Zify.PropUnOp.register t }
+| ["Add" "Zify" "BinOpSpec" reference(t) ] -> { Zify.BinOpSpec.register t }
+| ["Add" "Zify" "UnOpSpec"  reference(t) ] -> { Zify.UnOpSpec.register t }
+| ["Add" "Zify" "Saturate"  reference(t) ] -> { Zify.Saturate.register t }
 END
 
 TACTIC EXTEND ITER
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 800dc6cee2..2cb615170b 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -23,6 +23,19 @@ let zify str =
     (UnivGen.constr_of_monomorphic_global
        (Coqlib.lib_ref ("ZifyClasses." ^ str)))
 
+(** classes *)
+let coq_InjTyp = lazy (Coqlib.lib_ref "ZifyClasses.InjTyp")
+
+let coq_BinOp = lazy (Coqlib.lib_ref "ZifyClasses.BinOp")
+let coq_UnOp = lazy (Coqlib.lib_ref "ZifyClasses.UnOp")
+let coq_CstOp = lazy (Coqlib.lib_ref "ZifyClasses.CstOp")
+let coq_BinRel = lazy (Coqlib.lib_ref "ZifyClasses.BinRel")
+let coq_PropBinOp = lazy (Coqlib.lib_ref "ZifyClasses.PropBinOp")
+let coq_PropUOp = lazy (Coqlib.lib_ref "ZifyClasses.PropUOp")
+let coq_BinOpSpec = lazy (Coqlib.lib_ref "ZifyClasses.BinOpSpec")
+let coq_UnOpSpec = lazy (Coqlib.lib_ref "ZifyClasses.UnOpSpec")
+let coq_Saturate = lazy (Coqlib.lib_ref "ZifyClasses.Saturate")
+
 (* morphism like lemma *)
 
 let mkapp2 = lazy (zify "mkapp2")
@@ -46,7 +59,6 @@ let op_iff_morph = lazy (zify "iff_morph")
 let op_not = lazy (zify "not")
 let op_not_morph = lazy (zify "not_morph")
 let op_True = lazy (zify "True")
-let whd = Reductionops.clos_whd_flags CClosure.all
 
 (** [unsafe_to_constr c] returns a [Constr.t] without considering an evar_map.
     This is useful for calling Constr.hash *)
@@ -59,6 +71,7 @@ let gl_pr_constr e =
   let evd = Evd.from_env genv in
   pr_constr genv evd e
 
+let whd = Reductionops.clos_whd_flags CClosure.all
 let is_convertible env evd t1 t2 = Reductionops.(is_conv env evd t1 t2)
 
 (** [get_type_of] performs beta reduction ;
@@ -344,6 +357,7 @@ module type Elt = sig
   (** name *)
   val name : string
 
+  val gref : GlobRef.t Lazy.t
   val table : (term_kind * decl_kind) ConstrMap.t ref
   val cast : elt decl -> decl_kind
   val dest : decl_kind -> elt decl option
@@ -375,6 +389,7 @@ module EInj = struct
   type elt = EInjT.t
 
   let name = "EInj"
+  let gref = coq_InjTyp
   let table = table
   let cast x = InjTyp x
   let dest = function InjTyp x -> Some x | _ -> None
@@ -432,6 +447,7 @@ module EBinOp = struct
   open EBinOpT
 
   let name = "BinOp"
+  let gref = coq_BinOp
   let table = table
 
   let mk_elt evd i a =
@@ -473,6 +489,7 @@ module ECstOp = struct
   open ECstOpT
 
   let name = "CstOp"
+  let gref = coq_CstOp
   let table = table
   let cast x = CstOp x
   let dest = function CstOp x -> Some x | _ -> None
@@ -499,6 +516,7 @@ module EUnOp = struct
   open EUnOpT
 
   let name = "UnOp"
+  let gref = coq_UnOp
   let table = table
   let cast x = UnOp x
   let dest = function UnOp x -> Some x | _ -> None
@@ -531,6 +549,7 @@ module EBinRel = struct
   open EBinRelT
 
   let name = "BinRel"
+  let gref = coq_BinRel
   let table = table
   let cast x = BinRel x
   let dest = function BinRel x -> Some x | _ -> None
@@ -557,6 +576,7 @@ module EPropBinOp = struct
   open EPropBinOpT
 
   let name = "PropBinOp"
+  let gref = coq_PropBinOp
   let table = table
   let cast x = PropOp x
   let dest = function PropOp x -> Some x | _ -> None
@@ -569,7 +589,8 @@ module EPropUnOp = struct
 
   open EPropUnOpT
 
-  let name = "PropUnOp"
+  let name = "PropUOp"
+  let gref = coq_PropUOp
   let table = table
   let cast x = PropUnOp x
   let dest = function PropUnOp x -> Some x | _ -> None
@@ -580,7 +601,7 @@ end
 let constr_of_term_kind = function Application c -> c | OtherTerm c -> c
 
 module type S = sig
-  val register : Constrexpr.constr_expr -> unit
+  val register : Libnames.qualid -> unit
   val print : unit -> unit
 end
 
@@ -612,7 +633,7 @@ module MakeTable (E : Elt) = struct
     let c = EConstr.of_constr c in
     let t = get_type_of env evd c in
     match EConstr.kind evd t with
-    | App (intyp, args) ->
+    | App (intyp, args) when EConstr.isRefX evd (Lazy.force E.gref) intyp ->
       let styp = args.(E.get_key) in
       let elt = {decl = c; deriv = make_elt (evd, c)} in
       register_hint evd styp elt
@@ -621,10 +642,11 @@ module MakeTable (E : Elt) = struct
       raise
         (CErrors.user_err
            Pp.(
-             str ": Cannot register term "
-             ++ pr_constr env evd c ++ str ". It has type "
-             ++ pr_constr env evd t
-             ++ str " which should be of the form  [F X1 .. Xn]"))
+             str "Cannot register " ++ pr_constr env evd c
+             ++ str ". It has type " ++ pr_constr env evd t
+             ++ str " instead of type "
+             ++ Printer.pr_global (Lazy.force E.gref)
+             ++ str " X1 ... Xn"))
 
   let register_obj : Constr.constr -> Libobject.obj =
     let cache_constr (_, c) =
@@ -638,17 +660,19 @@ module MakeTable (E : Elt) = struct
          ("register-zify-" ^ E.name)
          ~cache:cache_constr ~subst:(Some subst_constr)
 
-  (** [register c] is called from the VERNACULAR ADD [name] constr(t).
+  (** [register c] is called from the VERNACULAR ADD [name] reference(t).
        The term [c] is interpreted and
        registered as a [superglobal_object_nodischarge].
        TODO: pre-compute [get_type_of] - [cache_constr] is using another environment.
      *)
   let register c =
-    let env = Global.env () in
-    let evd = Evd.from_env env in
-    let evd, c = Constrintern.interp_open_constr env evd c in
-    let _ = Lib.add_anonymous_leaf (register_obj (EConstr.to_constr evd c)) in
-    ()
+    try
+      let c = UnivGen.constr_of_monomorphic_global (Nametab.locate c) in
+      let _ = Lib.add_anonymous_leaf (register_obj c) in
+      ()
+    with Not_found ->
+      raise
+        (CErrors.user_err Pp.(Libnames.pr_qualid c ++ str " does not exist."))
 
   let pp_keys () =
     let env = Global.env () in
@@ -672,6 +696,7 @@ module ESat = struct
   open ESatT
 
   let name = "Saturate"
+  let gref = coq_Saturate
   let table = saturate
   let cast x = Saturate x
   let dest = function Saturate x -> Some x | _ -> None
@@ -685,6 +710,7 @@ module EUnopSpec = struct
   type elt = ESpecT.t
 
   let name = "UnopSpec"
+  let gref = coq_UnOpSpec
   let table = specs
   let cast x = UnOpSpec x
   let dest = function UnOpSpec x -> Some x | _ -> None
@@ -698,6 +724,7 @@ module EBinOpSpec = struct
   type elt = ESpecT.t
 
   let name = "BinOpSpec"
+  let gref = coq_BinOpSpec
   let table = specs
   let cast x = BinOpSpec x
   let dest = function BinOpSpec x -> Some x | _ -> None
diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli
index 555bb4c7fb..68f23393ee 100644
--- a/plugins/micromega/zify.mli
+++ b/plugins/micromega/zify.mli
@@ -7,10 +7,9 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
-open Constrexpr
 
 module type S = sig
-  val register : constr_expr -> unit
+  val register : Libnames.qualid -> unit
   val print : unit -> unit
 end
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 9480bbdc2e..f5768726c3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -98,8 +98,7 @@ let forward_feedback, forward_feedback_hook =
   let m = Mutex.create () in
   Hook.make ~default:(function
     | { doc_id = did; span_id = id; route; contents } ->
-        try Mutex.lock m; feedback ~did ~id ~route contents; Mutex.unlock m
-        with e -> Mutex.unlock m; raise e) ()
+        CThread.with_lock m ~scope:(fun () -> feedback ~did ~id ~route contents)) ()
 
 let unreachable_state, unreachable_state_hook = Hook.make
  ~default:(fun ~doc:_ _ _ -> ()) ()
@@ -758,17 +757,16 @@ end = struct (* {{{ *)
     let worker = ref None
 
     let set_last_job j =
-      Mutex.lock m;
-      job := Some j;
-      Condition.signal c;
-      Mutex.unlock m
+      CThread.with_lock m ~scope:(fun () ->
+          job := Some j;
+          Condition.signal c)
 
     let get_last_job () =
-      Mutex.lock m;
-      while Option.is_empty !job do Condition.wait c m; done;
-      match !job with
-      | None -> assert false
-      | Some x -> job := None; Mutex.unlock m; x
+      CThread.with_lock m ~scope:(fun () ->
+          while Option.is_empty !job do Condition.wait c m; done;
+          match !job with
+          | None -> assert false
+          | Some x -> job := None; x)
 
     let run_command () =
       try while true do get_last_job () () done
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index 2aaca85582..f5bd726dde 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -68,61 +68,54 @@ let create () = {
 
 let pop ?(picky=(fun _ -> true)) ?(destroy=ref false) tq =
   let { queue = q; lock = m; cond = c; cond_waiting = cn } = tq in
-  Mutex.lock m;
-  if tq.release then (Mutex.unlock m; raise BeingDestroyed);
-  while not (PriorityQueue.exists picky q || !destroy) do
-    tq.nwaiting <- tq.nwaiting + 1;
-    Condition.broadcast cn;
-    Condition.wait c m;
-    tq.nwaiting <- tq.nwaiting - 1;
-    if tq.release || !destroy then (Mutex.unlock m; raise BeingDestroyed)
-  done;
-  if !destroy then (Mutex.unlock m; raise BeingDestroyed);
-  let x = PriorityQueue.pop ~picky q in
-  Condition.signal c;
-  Condition.signal cn;
-  Mutex.unlock m;
-  x
+  CThread.with_lock m ~scope:(fun () ->
+      if tq.release then raise BeingDestroyed;
+      while not (PriorityQueue.exists picky q || !destroy) do
+        tq.nwaiting <- tq.nwaiting + 1;
+        Condition.broadcast cn;
+        Condition.wait c m;
+        tq.nwaiting <- tq.nwaiting - 1;
+        if tq.release || !destroy then raise BeingDestroyed
+      done;
+      if !destroy then raise BeingDestroyed;
+      let x = PriorityQueue.pop ~picky q in
+      Condition.signal c;
+      Condition.signal cn;
+      x)
 
 let broadcast tq =
   let { lock = m; cond = c } = tq in
-  Mutex.lock m;
-  Condition.broadcast c;
-  Mutex.unlock m
+  CThread.with_lock m ~scope:(fun () ->
+      Condition.broadcast c)
 
 let push tq x =
   let { queue = q; lock = m; cond = c; release } = tq in
   if release then CErrors.anomaly(Pp.str
     "TQueue.push while being destroyed! Only 1 producer/destroyer allowed.");
-  Mutex.lock m;
-  PriorityQueue.push q x;
-  Condition.broadcast c;
-  Mutex.unlock m
+  CThread.with_lock m ~scope:(fun () ->
+      PriorityQueue.push q x;
+      Condition.broadcast c)
 
 let length tq =
   let { queue = q; lock = m } = tq in
-  Mutex.lock m;
-  let n = PriorityQueue.length q in
-  Mutex.unlock m;
-  n
+  CThread.with_lock m ~scope:(fun () ->
+      PriorityQueue.length q)
 
 let clear tq =
   let { queue = q; lock = m; cond = c } = tq in
-  Mutex.lock m;
-  PriorityQueue.clear q;
-  Mutex.unlock m
+  CThread.with_lock m ~scope:(fun () ->
+      PriorityQueue.clear q)
 
 let clear_saving tq f =
   let { queue = q; lock = m; cond = c } = tq in
-  Mutex.lock m;
   let saved = ref [] in
-  while not (PriorityQueue.is_empty q) do
-    let elem = PriorityQueue.pop q in
-    match f elem with
-    | Some x -> saved := x :: !saved
-    | None -> ()
-  done;
-  Mutex.unlock m;
+  CThread.with_lock m ~scope:(fun () ->
+      while not (PriorityQueue.is_empty q) do
+        let elem = PriorityQueue.pop q in
+        match f elem with
+        | Some x -> saved := x :: !saved
+        | None -> ()
+      done);
   List.rev !saved
 
 let is_empty tq = PriorityQueue.is_empty tq.queue
@@ -130,32 +123,28 @@ let is_empty tq = PriorityQueue.is_empty tq.queue
 let destroy tq =
   tq.release <- true;
   while tq.nwaiting > 0 do
-    Mutex.lock tq.lock;
-    Condition.broadcast tq.cond;
-    Mutex.unlock tq.lock;
+    CThread.with_lock tq.lock ~scope:(fun () ->
+        Condition.broadcast tq.cond)
   done;
   tq.release <- false
 
 let wait_until_n_are_waiting_and_queue_empty j tq =
-  Mutex.lock tq.lock;
-  while not (PriorityQueue.is_empty tq.queue) || tq.nwaiting < j do
-    Condition.wait tq.cond_waiting tq.lock
-  done;
-  Mutex.unlock tq.lock
+  CThread.with_lock tq.lock ~scope:(fun () ->
+      while not (PriorityQueue.is_empty tq.queue) || tq.nwaiting < j do
+        Condition.wait tq.cond_waiting tq.lock
+      done)
 
 let wait_until_n_are_waiting_then_snapshot j tq =
   let l = ref [] in
-  Mutex.lock tq.lock;
-  while not (PriorityQueue.is_empty tq.queue) do
-    l := PriorityQueue.pop tq.queue :: !l
-  done;
-  while tq.nwaiting < j do Condition.wait tq.cond_waiting tq.lock done;
-  List.iter (PriorityQueue.push tq.queue) (List.rev !l);
-  if !l <> [] then Condition.broadcast tq.cond;
-  Mutex.unlock tq.lock;
+  CThread.with_lock tq.lock ~scope:(fun () ->
+      while not (PriorityQueue.is_empty tq.queue) do
+        l := PriorityQueue.pop tq.queue :: !l
+      done;
+      while tq.nwaiting < j do Condition.wait tq.cond_waiting tq.lock done;
+      List.iter (PriorityQueue.push tq.queue) (List.rev !l);
+      if !l <> [] then Condition.broadcast tq.cond);
   List.rev !l
 
 let set_order tq rel =
-  Mutex.lock tq.lock;
-  PriorityQueue.set_rel rel tq.queue;
-  Mutex.unlock tq.lock
+  CThread.with_lock tq.lock ~scope:(fun () ->
+      PriorityQueue.set_rel rel tq.queue)
diff --git a/stm/workerPool.ml b/stm/workerPool.ml
index 45c92c3748..fef9300377 100644
--- a/stm/workerPool.ml
+++ b/stm/workerPool.ml
@@ -72,12 +72,7 @@ let worker_handshake slave_ic slave_oc =
     exit 1
 
 let locking { lock; pool = p } f =
-  try
-    Mutex.lock lock;
-    let x = f p in
-    Mutex.unlock lock;
-    x
-  with e -> Mutex.unlock lock; raise e
+  CThread.with_lock lock ~scope:(fun () -> f p)
 
 let rec create_worker extra pool priority id =
   let cancel = ref false in
diff --git a/test-suite/micromega/bug_14054.v b/test-suite/micromega/bug_14054.v
new file mode 100644
index 0000000000..d97e13375f
--- /dev/null
+++ b/test-suite/micromega/bug_14054.v
@@ -0,0 +1,46 @@
+(* bug 13242 *)
+
+Require Import Lia.
+Fail Add Zify InjTyp id.
+
+(* bug 14054 *)
+
+Require Import Coq.ZArith.ZArith. Open Scope Z_scope.
+Require Coq.Init.Byte .
+Require Import Coq.micromega.ZifyClasses Coq.micromega.Lia.
+
+Notation byte := Coq.Init.Byte.byte.
+
+Module byte.
+  Definition unsigned(b: byte): Z := Z.of_N (Byte.to_N b).
+End byte.
+
+Section WithA.
+  Context (A: Type).
+  Fixpoint tuple(n: nat): Type :=
+    match n with
+    | O => unit
+    | S m => A * tuple m
+    end.
+End WithA.
+
+Module LittleEndian.
+  Fixpoint combine (n : nat) : forall (bs : tuple byte n), Z :=
+    match n with
+    | O => fun _ => 0
+    | S n => fun bs => Z.lor (byte.unsigned (fst bs))
+                             (Z.shiftl (combine n (snd bs)) 8)
+    end.
+  Lemma combine_bound: forall {n: nat} (t: tuple byte n),
+      0 <= LittleEndian.combine n t < 2 ^ (8 * Z.of_nat n).
+  Admitted.
+End LittleEndian.
+
+Instance InjByteTuple{n: nat}: InjTyp (tuple byte n) Z := {|
+  inj := LittleEndian.combine n;
+  pred x := 0 <= x < 2 ^ (8 * Z.of_nat n);
+  cstr := @LittleEndian.combine_bound n;
+|}.
+Fail Add Zify InjTyp InjByteTuple.
+Fail Add Zify UnOp InjByteTuple.
+Fail Add Zify UnOp X.
diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v
index f6ade67c5f..a08a56b20e 100644
--- a/theories/micromega/ZifyClasses.v
+++ b/theories/micromega/ZifyClasses.v
@@ -250,8 +250,18 @@ Register rew_iff     as ZifyClasses.rew_iff.
 Register source_prop as ZifyClasses.source_prop.
 Register injprop_ok  as ZifyClasses.injprop_ok.
 Register iff         as ZifyClasses.iff.
+
+Register InjTyp      as ZifyClasses.InjTyp.
+Register BinOp       as ZifyClasses.BinOp.
+Register UnOp        as ZifyClasses.UnOp.
+Register CstOp       as ZifyClasses.CstOp.
+Register BinRel      as ZifyClasses.BinRel.
+Register PropOp   as ZifyClasses.PropOp.
+Register PropUOp     as ZifyClasses.PropUOp.
 Register BinOpSpec   as ZifyClasses.BinOpSpec.
 Register UnOpSpec    as ZifyClasses.UnOpSpec.
+Register Saturate    as ZifyClasses.Saturate.
+
 
 (** Propositional logic *)
 Register and as ZifyClasses.and.
diff --git a/tools/coqdoc/dune b/tools/coqdoc/dune
index cc888a959f..432d88b2ff 100644
--- a/tools/coqdoc/dune
+++ b/tools/coqdoc/dune
@@ -5,6 +5,13 @@
   (coqdoc.css as tools/coqdoc/coqdoc.css)
   (coqdoc.sty as tools/coqdoc/coqdoc.sty)))
 
+; File needs to be here too.
+(install
+ (section share)
+ (package coq-core)
+ (files
+  (coqdoc.sty as texmf/tex/latex/misc/coqdoc.sty)))
+
 (executable
  (name main)
  (public_name coqdoc)