Fix conflicts with latest master.

46 files changed, 354 insertions, 193 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 31bfebc3d5..6d307b3c5e 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -263,6 +263,7 @@ let raw_intern_library f =
 type summary_disk = {
   md_name : compilation_unit_name;
   md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
+  md_ocaml : string;
 }
 
 module Dyn = Dyn.Make ()
@@ -345,6 +346,7 @@ let intern_from_file ~intern_mode (dir, f) =
       let () = close_in ch in
       let ch = open_in_bin f in
       let () = close_in ch in
+      let () = System.check_caml_version ~caml:sd.md_ocaml ~file:f in
       if dir <> sd.md_name then
         user_err ~hdr:"intern_from_file"
           (name_clash_message dir sd.md_name f);
diff --git a/checker/values.ml b/checker/values.ml
index 76e3ab0d45..cce0ce7203 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -435,7 +435,7 @@ let v_stm_seg = v_pair v_tasks v_counters
 (** Toplevel structures in a vo (see Cic.mli) *)
 
 let v_libsum =
-  Tuple ("summary", [|v_dp;v_deps|])
+  Tuple ("summary", [|v_dp;v_deps;String|])
 
 let v_lib =
   Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index b87a9c0392..5f7d0b5789 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -351,3 +351,10 @@
 : "${metacoq_CI_REF:=master}"
 : "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}"
 : "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}"
+
+########################################################################
+# SF suite
+########################################################################
+: "${sf_CI_REF:=master}"
+: "${sf_CI_GITURL:=https://github.com/DeepSpec/sf}"
+: "${sf_CI_ARCHIVEURL:=${sf_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index b9d6215e60..d46e53717f 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -3,22 +3,9 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-CIRCLE_SF_TOKEN=00127070c10f5f09574b050e4f08e924764680d2
+git_download sf
 
-# "latest" is disabled due to lack of build credits upstream, thus artifacts fail
-# data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
-data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/1411/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
-
-mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}"
-
-sf_lf_CI_TARURL=$(echo "$data"  | jq -rc '.[] | select (.path == "lf.tgz") | .url')
-sf_plf_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "plf.tgz") | .url')
-sf_vfa_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "vfa.tgz") | .url')
-
-wget -O - "${sf_lf_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz
-wget -O - "${sf_plf_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz
-wget -O - "${sf_vfa_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz
-
-( cd lf  && make clean && make )
-( cd plf && make clean && make )
-( cd vfa && make clean && make )
+( cd lf-current  && make clean && make )
+( cd plf-current && make clean && make )
+( cd vfa-current && make clean && make )
+# ( cd qc-current && make clean && make )
diff --git a/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh b/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh
new file mode 100644
index 0000000000..50eaf0b109
--- /dev/null
+++ b/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "8808" ] || [ "$CI_BRANCH" = "master+support-binder+term-in-abbrev" ]; then
+
+    elpi_CI_REF=master+adapt-coq8808-syndef-same-expressiveness-notation
+    elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+fi
diff --git a/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst b/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst
new file mode 100644
index 0000000000..e1fcfb78c4
--- /dev/null
+++ b/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Abbreviations support arguments occurring both in term and binder position
+  (`#8808 <https://github.com/coq/coq/pull/8808>`_,
+  by Hugo Herbelin).
diff --git a/doc/changelog/08-tools/11851-coqc-flags-fix.rst b/doc/changelog/08-tools/11851-coqc-flags-fix.rst
index a07e48d2d8..ff736641b4 100644
--- a/doc/changelog/08-tools/11851-coqc-flags-fix.rst
+++ b/doc/changelog/08-tools/11851-coqc-flags-fix.rst
@@ -1,6 +1,9 @@
 - **Changed:**
-  The order in which the require/load flags `-l`, `-ri`, `-re`, `-rfrom`, etc.
-  and the option set flags `-set`, `-unset` are processed have been reversed.
-  In the new behavior, require/load flags are processed before option flags.
-  (`#11851 <https://github.com/coq/coq/pull/11851>`_,
+  The order in which the require flags `-ri`, `-re`, `-rfrom`, etc.
+  and the option flags `-set`, `-unset` are given now matters.  In
+  particular, it is now possible to interleave the loading of plugins
+  and the setting of options by choosing the right order for these
+  flags.  The load flags `-l` and `-lv` are still processed afterward
+  for now (`#11851 <https://github.com/coq/coq/pull/11851>`_ and
+  `#12097 <https://github.com/coq/coq/pull/12097>`_,
   by Lasse Blaauwbroek).
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 58fd49c390..d4ceffac9f 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -151,7 +151,7 @@ and ``coqtop``, unless stated otherwise:
   while processing options such as -R and -Q. By default, only the
   conventional version control management directories named CVS
   and_darcs are excluded.
-:-nois: Start from an empty state instead of loading the Init.Prelude
+:-nois, -noinit: Start from an empty state instead of loading the `Init.Prelude`
   module.
 :-init-file *file*: Load *file* as the resource file instead of
   loading the default resource file from the standard configuration
@@ -163,26 +163,53 @@ and ``coqtop``, unless stated otherwise:
   |Coq| script from *file.v*. Write its contents to the standard output as
   it is executed.
 :-load-vernac-object *qualid*: Load |Coq| compiled library :n:`@qualid`. This
-  is equivalent to running :cmd:`Require` :n:`qualid`.
+  is equivalent to running :cmd:`Require` :n:`@qualid`.
+
+  .. _interleave-command-line:
+
+  .. note::
+
+     Note that the relative order of this command-line option and its
+     variants (`-rfrom`, `-ri`, `-re`, etc.)  and of the `-set` and
+     `-unset` options matters since the various :cmd:`Require`,
+     :cmd:`Require Import`, :cmd:`Require Export`, :cmd:`Set` and
+     :cmd:`Unset` commands will be executed in the order specified on
+     the command-line.
+
 :-rfrom *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid`.
-  This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`.
+  This is equivalent to running :cmd:`From <From ... Require>`
+  :n:`@dirpath` :cmd:`Require <From ... Require>` :n:`@qualid`.
+  See the :ref:`note above <interleave-command-line>` regarding the order
+  of command-line options.
 :-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it.
   This is equivalent to running :cmd:`Require Import` :n:`@qualid`.
+  See the :ref:`note above <interleave-command-line>` regarding the order
+  of command-line options.
 :-re *qualid*, -require-export *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it.
   This is equivalent to running :cmd:`Require Export` :n:`@qualid`.
-:-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and import it.
-  This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`.
-:-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it.
-  This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Export` :n:`@qualid`.
+  See the :ref:`note above <interleave-command-line>` regarding the order
+  of command-line options.
+:-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*:
+  Load |Coq| compiled library :n:`@qualid` and import it.  This is
+  equivalent to running :cmd:`From <From ... Require>` :n:`@dirpath`
+  :cmd:`Require Import <From ... Require>` :n:`@qualid`.  See the
+  :ref:`note above <interleave-command-line>` regarding the order of
+  command-line options.
+:-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*:
+  Load |Coq| compiled library :n:`@qualid` and transitively import it.
+  This is equivalent to running :cmd:`From <From ... Require>`
+  :n:`@dirpath` :cmd:`Require Export <From ... Require>` :n:`@qualid`.
+  See the :ref:`note above <interleave-command-line>` regarding the
+  order of command-line options.
 :-batch: Exit just after argument parsing. Available for ``coqtop`` only.
 :-verbose: Output the content of the input file as it is compiled.
   This option is available for ``coqc`` only.
 :-vos: Indicate |Coq| to skip the processing of opaque proofs
-  (i.e., proofs ending with ``Qed`` or ``Admitted``), output a ``.vos`` files
+  (i.e., proofs ending with :cmd:`Qed` or :cmd:`Admitted`), output a ``.vos`` files
   instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files
-  when interpreting ``Require`` commands.
+  when interpreting :cmd:`Require` commands.
 :-vok: Indicate |Coq| to check a file completely, to load ``.vos`` files instead
-  of ``.vo`` files when interpreting ``Require`` commands, and to output an empty
+  of ``.vo`` files when interpreting :cmd:`Require` commands, and to output an empty
   ``.vok`` files upon success instead of writing a ``.vo`` file.
 :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This
   option expects all, none or a comma-separated list of warning names or
@@ -192,7 +219,7 @@ and ``coqtop``, unless stated otherwise:
   the output channel supports ANSI escape sequences.
 :-diffs (on|off|removed): *Coqtop only*.  Controls highlighting of differences
   between proof steps.  ``on`` highlights added tokens, ``removed`` highlights both added and
-  removed tokens.  Requires that ``–color`` is enabled.  (see Section
+  removed tokens.  Requires that ``-color`` is enabled.  (see Section
   :ref:`showing_diffs`).
 :-beautify: Pretty-print each command to *file.beautified* when
   compiling *file.v*, in order to get old-fashioned
@@ -218,17 +245,25 @@ and ``coqtop``, unless stated otherwise:
   changes in the auto-generated name scheme. The options are provided to
   facilitate tracking down problems.
 :-set *string*: Enable flags and set options. *string* should be
-   ``Option Name=value``, the value is interpreted according to the
-   type of the option. For flags ``Option Name`` is equivalent to
-   ``Option Name=true``. For instance ``-set "Universe Polymorphism"``
+   :n:`@setting_name=value`, the value is interpreted according to the
+   type of the option. For flags :n:`@setting_name` is equivalent to
+   :n:`@setting_name=true`. For instance ``-set "Universe Polymorphism"``
    will enable :flag:`Universe Polymorphism`. Note that the quotes are
-   shell syntax, Coq does not see them. Flags are processed after initialization
-   of the document. This includes the `Prelude` if loaded and any libraries loaded
-   through the `-l`, `-lv`, `-r`, `-re`, `-ri`, `rfrom`, `-refrom` and `-rifrom`
-   options.
+   shell syntax, Coq does not see them.
+   See the :ref:`note above <interleave-command-line>` regarding the order
+   of command-line options.
 :-unset *string*: As ``-set`` but used to disable options and flags.
-:-compat *version*: Attempt to maintain some backward-compatibility
-  with a previous version.
+  *string* must be :n:`"@setting_name"`.
+  See the :ref:`note above <interleave-command-line>` regarding the order
+  of command-line options.
+:-compat *version*: Load a file that sets a few options to maintain
+  partial backward-compatibility with a previous version.  This is
+  equivalent to :cmd:`Require Import` `Coq.Compat.CoqXXX` with `XXX`
+  one of the last three released versions (including the current
+  version).  Note that the :ref:`explanations above
+  <interleave-command-line>` regarding the order of command-line
+  options apply, and this could be relevant if you are resetting some
+  of the compatibility options.
 :-dump-glob *file*: Dump references for global names in file *file*
   (to be used by coqdoc, see :ref:`coqdoc`). By default, if *file.v* is being
   compiled, *file.glob* is used.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 8d1d46676c..976f79d7b7 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -618,6 +618,41 @@ the next command fails because p does not bind in the instance of n.
    Notation "[> a , .. , b <]" :=
      (cons a .. (cons b nil) .., cons b .. (cons a nil) ..).
 
+Notations with expressions used both as binder and term
++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+
+It is possible to use parameters of the notation both in term and
+binding position. Here is an example:
+
+.. coqtop:: in
+
+   Definition force n (P:nat -> Prop) := forall n', n' >= n -> P n'.
+   Notation "▢_ n P" := (force n (fun n => P))
+     (at level 0, n ident, P at level 9, format "▢_ n  P").
+
+.. coqtop:: all
+
+   Check exists p, ▢_p (p >= 1).
+
+More generally, the parameter can be a pattern, as in the following
+variant:
+
+.. coqtop:: in reset
+
+   Definition force2 q (P:nat*nat -> Prop) :=
+     (forall n', n' >= fst q -> forall p', p' >= snd q -> P q).
+
+   Notation "▢_ p P" := (force2 p (fun p => P))
+     (at level 0, p pattern at level 0, P at level 9, format "▢_ p  P").
+
+.. coqtop:: all
+
+   Check exists x y, ▢_(x,y) (x >= 1 /\ y >= 2).
+
+This support is experimental. For instance, the notation is used for
+printing only if the occurrence of the parameter in term position
+comes in the right-hand side before the occurrence in binding position.
+
 .. _RecursiveNotations:
 
 Notations with recursive patterns
@@ -1383,6 +1418,17 @@ Abbreviations
    exception, if the right-hand side is just of the form :n:`@@qualid`,
    this conventionally stops the inheritance of implicit arguments.
 
+   Like for notations, it is possible to bind binders in
+   abbreviations. Here is an example:
+
+   .. coqtop:: in reset
+
+      Definition force2 q (P:nat*nat -> Prop) :=
+        (forall n', n' >= fst q -> forall p', p' >= snd q -> P q).
+
+      Notation F p P := (force2 p (fun p => P)).
+      Check exists x y, F (x,y) (x >= 1 /\ y >= 2).
+
 .. extracted from Gallina chapter
 
 Numerals and strings
diff --git a/engine/uState.ml b/engine/uState.ml
index 00649ce042..99ac5f2ce8 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -34,7 +34,7 @@ type t =
    (** The subset of unification variables that can be instantiated with
         algebraic universes as they appear in inferred types only. *)
    uctx_universes : UGraph.t; (** The current graph extended with the local constraints *)
-   uctx_universes_lbound : Univ.Level.t; (** The lower bound on universes (e.g. Set or Prop) *)
+   uctx_universes_lbound : UGraph.Bound.t; (** The lower bound on universes (e.g. Set or Prop) *)
    uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *)
    uctx_weak_constraints : UPairSet.t
  }
@@ -48,7 +48,7 @@ let empty =
     uctx_univ_variables = LMap.empty;
     uctx_univ_algebraic = LSet.empty;
     uctx_universes = initial_sprop_cumulative;
-    uctx_universes_lbound = Univ.Level.set;
+    uctx_universes_lbound = UGraph.Bound.Set;
     uctx_initial_universes = initial_sprop_cumulative;
     uctx_weak_constraints = UPairSet.empty; }
 
@@ -443,6 +443,10 @@ let check_univ_decl ~poly uctx decl =
       (ContextSet.constraints uctx.uctx_local);
   ctx
 
+let is_bound l lbound = match lbound with
+| UGraph.Bound.Prop -> Level.is_prop l
+| UGraph.Bound.Set -> Level.is_set l
+
 let restrict_universe_context ~lbound (univs, csts) keep =
   let removed = LSet.diff univs keep in
   if LSet.is_empty removed then univs, csts
@@ -455,7 +459,7 @@ let restrict_universe_context ~lbound (univs, csts) keep =
   let allkept = LSet.union (UGraph.domain UGraph.initial_universes) (LSet.diff allunivs removed) in
   let csts = UGraph.constraints_for ~kept:allkept g in
   let csts = Constraint.filter (fun (l,d,r) ->
-      not ((Level.equal l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in
+      not ((is_bound l lbound && d == Le) || (Level.is_prop l && d == Lt && Level.is_set r))) csts in
   (LSet.inter univs keep, csts)
 
 let restrict ctx vars =
@@ -600,10 +604,10 @@ let make_with_initial_binders ~lbound e us =
 
 let add_global_univ uctx u =
   let initial =
-    UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_initial_universes
+    UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.uctx_initial_universes
   in
   let univs =
-    UGraph.add_universe ~lbound:Univ.Level.set ~strict:true u uctx.uctx_universes
+    UGraph.add_universe ~lbound:UGraph.Bound.Set ~strict:true u uctx.uctx_universes
   in
   { uctx with uctx_local = ContextSet.add_universe u uctx.uctx_local;
                                      uctx_initial_universes = initial;
diff --git a/engine/uState.mli b/engine/uState.mli
index 6707826aae..533a501b59 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -25,9 +25,9 @@ type t
 
 val empty : t
 
-val make : lbound:Univ.Level.t -> UGraph.t -> t
+val make : lbound:UGraph.Bound.t -> UGraph.t -> t
 
-val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> lident list -> t
+val make_with_initial_binders : lbound:UGraph.Bound.t -> UGraph.t -> lident list -> t
 
 val is_empty : t -> bool
 
@@ -90,7 +90,7 @@ val universe_of_name : t -> Id.t -> Univ.Level.t
    the universes in [keep]. The constraints [csts] are adjusted so
    that transitive constraints between remaining universes (those in
    [keep] and those not in [univs]) are preserved. *)
-val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t
+val restrict_universe_context : lbound:UGraph.Bound.t -> ContextSet.t -> LSet.t -> ContextSet.t
 
 (** [restrict uctx ctx] restricts the local universes of [uctx] to
    [ctx] extended by local named universes and side effect universes
diff --git a/engine/univMinim.ml b/engine/univMinim.ml
index c05a7a800d..4dd7fe7e70 100644
--- a/engine/univMinim.ml
+++ b/engine/univMinim.ml
@@ -267,12 +267,16 @@ let minimize_univ_variables ctx us algs left right cstrs =
 module UPairs = OrderedType.UnorderedPair(Univ.Level)
 module UPairSet = Set.Make (UPairs)
 
+let is_bound l lbound = match lbound with
+| UGraph.Bound.Prop -> Level.is_prop l
+| UGraph.Bound.Set -> Level.is_set l
+
 (* TODO check is_small/sprop *)
 let normalize_context_set ~lbound g ctx us algs weak =
   let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in
   (* Keep the Prop/Set <= i constraints separate for minimization *)
   let smallles, csts =
-    Constraint.partition (fun (l,d,r) -> d == Le && (Level.equal l lbound || Level.is_sprop l)) csts
+    Constraint.partition (fun (l,d,r) -> d == Le && (is_bound l lbound || Level.is_sprop l)) csts
   in
   let smallles = if get_set_minimization ()
     then Constraint.filter (fun (l,d,r) -> LMap.mem r us && not (Level.is_sprop l)) smallles
@@ -299,7 +303,7 @@ let normalize_context_set ~lbound g ctx us algs weak =
   (* We ignore the trivial Prop/Set <= i constraints. *)
   let noneqs =
     Constraint.filter
-      (fun (l,d,r) -> not ((d == Le && Level.equal l lbound) ||
+      (fun (l,d,r) -> not ((d == Le && is_bound l lbound) ||
                            (Level.is_prop l && d == Lt && Level.is_set r)))
       csts
   in
diff --git a/engine/univMinim.mli b/engine/univMinim.mli
index 2a46d87609..58853e47b8 100644
--- a/engine/univMinim.mli
+++ b/engine/univMinim.mli
@@ -25,7 +25,7 @@ module UPairSet : CSet.S with type elt = (Level.t * Level.t)
     (a global one if there is one) and transitively saturate
     the constraints w.r.t to the equalities. *)
 
-val normalize_context_set : lbound:Univ.Level.t -> UGraph.t -> ContextSet.t ->
+val normalize_context_set : lbound:UGraph.Bound.t -> UGraph.t -> ContextSet.t ->
   universe_opt_subst (* The defined and undefined variables *) ->
   LSet.t (* univ variables that can be substituted by algebraics *) ->
   UPairSet.t (* weak equality constraints *) ->
diff --git a/engine/univops.mli b/engine/univops.mli
index 02a731ad49..d0145f5643 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -15,5 +15,5 @@ open Univ
 val universes_of_constr : constr -> LSet.t
 [@@ocaml.deprecated "Use [Vars.universes_of_constr]"]
 
-val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t -> ContextSet.t
+val restrict_universe_context : lbound:UGraph.Bound.t -> ContextSet.t -> LSet.t -> ContextSet.t
 [@@ocaml.deprecated "Use [UState.restrict_universe_context]"]
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f82783f47d..9d0552817f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -976,10 +976,6 @@ let split_by_type_pat ?loc ids subst =
   assert (terms = [] && termlists = []);
   subst
 
-let make_subst ids l =
-  let fold accu (id, scopes) a = Id.Map.add id (a, scopes) accu in
-  List.fold_left2 fold Id.Map.empty ids l
-
 let intern_notation intern env ntnvars loc ntn fullargs =
   (* Adjust to parsing of { } *)
   let ntn,fullargs = contract_curly_brackets ntn fullargs in
@@ -1113,8 +1109,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
       if List.length args < nids then error_not_enough_arguments ?loc;
       let args1,args2 = List.chop nids args in
       check_no_explicitation args1;
-      let terms = make_subst ids (List.map fst args1) in
-      let subst = (terms, Id.Map.empty, Id.Map.empty, Id.Map.empty) in
+      let subst = split_by_type ids (List.map fst args1,[],[],[]) in
       let infos = (Id.Map.empty, env) in
       let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in
       let loc = c.loc in
@@ -1624,8 +1619,8 @@ let drop_notations_pattern looked_for genv =
               let nvars = List.length vars in
               if List.length pats < nvars then error_not_enough_arguments ?loc:qid.loc;
               let pats1,pats2 = List.chop nvars pats in
-              let subst = make_subst vars pats1 in
-              let idspl1 = List.map (in_not false qid.loc scopes (subst, Id.Map.empty) []) args in
+              let subst = split_by_type_pat vars (pats1,[]) in
+              let idspl1 = List.map (in_not false qid.loc scopes subst []) args in
               let (_,argscs) = find_remaining_scopes pats1 pats2 g in
               Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2)
         | _ -> raise Not_found
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 7184f5ea29..bd3e234a91 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Util
 open Pp
 open CErrors
 open Names
@@ -82,16 +81,9 @@ let in_syntax_constant : (bool * syndef) -> obj =
     subst_function = subst_syntax_constant;
     classify_function = classify_syntax_constant }
 
-type syndef_interpretation = (Id.t * subscopes) list * notation_constr
-
-(* Coercions to the general format of notation that also supports
-   variables bound to list of expressions *)
-let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,((Constrexpr.InConstrEntrySomeLevel,sc),NtnTypeConstr))) ids,ac)
-let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac)
-
 let declare_syntactic_definition ~local deprecation id ~onlyparsing pat =
   let syndef =
-    { syndef_pattern = in_pat pat;
+    { syndef_pattern = pat;
       syndef_onlyparsing = onlyparsing;
       syndef_deprecation = deprecation;
     }
@@ -106,14 +98,12 @@ let warn_deprecated_syntactic_definition =
 
 let search_syntactic_definition ?loc kn =
   let syndef = KNmap.find kn !syntax_table in
-  let def = out_pat syndef.syndef_pattern in
   Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation;
-  def
+  syndef.syndef_pattern
 
 let search_filtered_syntactic_definition ?loc filter kn =
   let syndef = KNmap.find kn !syntax_table in
-  let def = out_pat syndef.syndef_pattern in
-  let res = filter def in
+  let res = filter syndef.syndef_pattern in
   if Option.has_some res then
     Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation;
   res
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 8b323462a1..66a3132f2a 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -13,12 +13,10 @@ open Notation_term
 
 (** Syntactic definitions. *)
 
-type syndef_interpretation = (Id.t * subscopes) list * notation_constr
-
 val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t ->
-  onlyparsing:bool -> syndef_interpretation -> unit
+  onlyparsing:bool -> interpretation -> unit
 
-val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation
+val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> interpretation
 
 val search_filtered_syntactic_definition : ?loc:Loc.t ->
-  (syndef_interpretation -> 'a option) -> KerName.t -> 'a option
+  (interpretation -> 'a option) -> KerName.t -> 'a option
diff --git a/kernel/environ.ml b/kernel/environ.ml
index d6d52dbc2b..182ed55d0e 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -67,7 +67,7 @@ end
 type stratification = {
   env_universes : UGraph.t;
   env_sprop_allowed : bool;
-  env_universes_lbound : Univ.Level.t;
+  env_universes_lbound : UGraph.Bound.t;
   env_engagement : engagement
 }
 
@@ -129,7 +129,7 @@ let empty_env = {
   env_stratification = {
     env_universes = UGraph.initial_universes;
     env_sprop_allowed = true;
-    env_universes_lbound = Univ.Level.set;
+    env_universes_lbound = UGraph.Bound.Set;
     env_engagement = PredicativeSet };
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.empty;
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 7a46538772..79e632daa0 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -62,7 +62,7 @@ end
 type stratification = {
   env_universes : UGraph.t;
   env_sprop_allowed : bool;
-  env_universes_lbound : Univ.Level.t;
+  env_universes_lbound : UGraph.Bound.t;
   env_engagement : engagement
 }
 
@@ -96,8 +96,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool
 val empty_env : env
 
 val universes     : env -> UGraph.t
-val universes_lbound : env -> Univ.Level.t
-val set_universes_lbound : env -> Univ.Level.t -> env
+val universes_lbound : env -> UGraph.Bound.t
+val set_universes_lbound : env -> UGraph.Bound.t -> env
 val rel_context   : env -> Constr.rel_context
 val named_context : env -> Constr.named_context
 val named_context_val : env -> named_context_val
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 8ac96a6481..e9687991c0 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -321,7 +321,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
       if has_template_poly then
         (* For that particular case, we typecheck the inductive in an environment
            where the universes introduced by the definition are only [>= Prop] *)
-        let env = set_universes_lbound env Univ.Level.prop in
+        let env = set_universes_lbound env UGraph.Bound.Prop in
         push_context_set ~strict:false ctx env
       else
         (* In the regular case, all universes are [> Set] *)
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 5f5f0ef8cd..927db9e9e6 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -148,8 +148,14 @@ let enforce_leq_alg u v g =
   assert (check_leq g u v);
   cg
 
+module Bound =
+struct
+  type t = Prop | Set
+end
+
 exception AlreadyDeclared = G.AlreadyDeclared
 let add_universe u ~lbound ~strict g =
+  let lbound = match lbound with Bound.Prop -> Level.prop | Bound.Set -> Level.set in
   let graph = G.add u g.graph in
   let d = if strict then Lt else Le in
   enforce_constraint (lbound,d,u) {g with graph}
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 8d9afb0990..c9fbd7f694 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -48,7 +48,13 @@ val enforce_leq_alg : Universe.t -> Universe.t -> t -> Constraint.t * t
 
 exception AlreadyDeclared
 
-val add_universe : Level.t -> lbound:Level.t -> strict:bool -> t -> t
+module Bound :
+sig
+  type t = Prop | Set
+  (** The [Prop] bound is only used for template polymorphic inductive types. *)
+end
+
+val add_universe : Level.t -> lbound:Bound.t -> strict:bool -> t -> t
 
 (** Add a universe without (Prop,Set) <= u *)
 val add_universe_unconstrained : Level.t -> t -> t
@@ -86,7 +92,7 @@ val constraints_for : kept:LSet.t -> t -> Constraint.t
 val domain : t -> LSet.t
 (** Known universes *)
 
-val check_subtype : lbound:Level.t -> AUContext.t check_function
+val check_subtype : lbound:Bound.t -> AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
     [ctx1]. *)
 
diff --git a/lib/system.ml b/lib/system.ml
index 4e98651d6e..e25f758865 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -168,6 +168,15 @@ let try_remove filename =
 let error_corrupted file s =
   CErrors.user_err ~hdr:"System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
 
+let check_caml_version ~caml:s ~file:f =
+  if not (String.equal Coq_config.caml_version s) then
+    CErrors.user_err (str ("The file " ^ f ^ " was compiled with OCaml") ++
+    spc () ++ str s ++ spc () ++ str "while this instance of Coq was compiled \
+    with OCaml" ++ spc() ++ str Coq_config.caml_version ++ str "." ++ spc () ++
+    str "Coq object files need to be compiled with the same OCaml toolchain to \
+    be compatible.")
+  else ()
+
 let input_binary_int f ch =
   try input_binary_int ch
   with
diff --git a/lib/system.mli b/lib/system.mli
index 4a8c35b6ea..1e2f519327 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -88,6 +88,8 @@ val with_magic_number_check : ('a -> 'b) -> 'a -> 'b
 val marshal_out : out_channel -> 'a -> unit
 val marshal_in : string -> in_channel -> 'a
 
+val check_caml_version : caml:string -> file:string -> unit
+
 (** {6 Time stamps.} *)
 
 type time
diff --git a/library/global.mli b/library/global.mli
index 2acd7e2a67..2767594171 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -22,7 +22,7 @@ val env : unit -> Environ.env
 val env_is_initial : unit -> bool
 
 val universes : unit -> UGraph.t
-val universes_lbound : unit -> Univ.Level.t
+val universes_lbound : unit -> UGraph.Bound.t
 val named_context_val : unit -> Environ.named_context_val
 val named_context : unit -> Constr.named_context
 
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index ee2c87d19a..0f8d941b41 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1897,8 +1897,6 @@ type provername = string * int option
   * The caching mechanism.
   *)
 
-open Persistent_cache
-
 module MakeCache (T : sig
   type prover_option
   type coeff
@@ -1922,7 +1920,7 @@ struct
       Hash.((hash_pair T.hash_prover_option (List.fold_left hash_cstr)) 0)
   end
 
-  include PHashtable (E)
+  include Persistent_cache.PHashtable (E)
 
   let memo_opt use_cache cache_file f =
     let memof = memo cache_file f in
diff --git a/stm/stm.ml b/stm/stm.ml
index 5790bfc07e..b296f8f08f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2576,6 +2576,21 @@ end (* }}} *)
 (******************************************************************************)
 
 (** STM initialization options: *)
+
+type option_command = OptionSet of string option | OptionUnset
+
+type injection_command =
+  | OptionInjection of (Goptions.option_name * option_command)
+  (** Set flags or options before the initial state is ready. *)
+  | RequireInjection of (string * string option * bool option)
+  (** Require libraries before the initial state is
+     ready. Parameters follow [Library], that is to say,
+     [lib,prefix,import_export] means require library [lib] from
+     optional [prefix] and [import_export] if [Some false/Some true]
+     is used.  *)
+  (* -load-vernac-source interleaving is not supported yet *)
+  (* | LoadInjection of (string * bool) *)
+
 type stm_init_options =
   { doc_type : stm_doc_type
   (** The STM does set some internal flags differently depending on
@@ -2589,12 +2604,9 @@ type stm_init_options =
   (** [vo] load paths for the document. Usually extracted from -R
      options / _CoqProject *)
 
-  ; require_libs : (string * string option * bool option) list
-  (** Require [require_libs] before the initial state is
-     ready. Parameters follow [Library], that is to say,
-     [lib,prefix,import_export] means require library [lib] from
-     optional [prefix] and [import_export] if [Some false/Some true]
-     is used.  *)
+  ; injections : injection_command list
+  (** Injects Require and Set/Unset commands before the initial
+     state is ready *)
 
   ; stm_options  : AsyncOpts.stm_opt
   (** Low-level STM options *)
@@ -2625,13 +2637,51 @@ let dirpath_of_file f =
   let ldir = Libnames.add_dirpath_suffix ldir0 id in
   ldir
 
-let new_doc { doc_type ; ml_load_path; vo_load_path; require_libs; stm_options } =
+let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } =
 
   let require_file (dir, from, exp) =
     let mp = Libnames.qualid_of_string dir in
     let mfrom = Option.map Libnames.qualid_of_string from in
     Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
 
+  let interp_set_option opt v old =
+    let open Goptions in
+    let err expect =
+      let opt = String.concat " " opt in
+      let got = v in (* avoid colliding with Pp.v *)
+      CErrors.user_err
+        Pp.(str "-set: " ++ str opt ++
+            str" expects " ++ str expect ++
+            str" but got " ++ str got)
+    in
+    match old with
+    | BoolValue _ ->
+      let v = match String.trim v with
+        | "true" -> true
+        | "false" | "" -> false
+        | _ -> err "a boolean"
+      in
+      BoolValue v
+    | IntValue _ ->
+      let v = String.trim v in
+      let v = match int_of_string_opt v with
+        | Some _ as v -> v
+        | None -> if v = "" then None else err "an int"
+      in
+      IntValue v
+    | StringValue _ -> StringValue v
+    | StringOptValue _ -> StringOptValue (Some v) in
+
+  let set_option = let open Goptions in function
+      | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt
+      | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true
+      | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v in
+
+  let handle_injection = function
+    | RequireInjection r -> require_file r
+    (* | LoadInjection l -> *)
+    | OptionInjection o -> set_option o in
+
   (* Set the options from the new documents *)
   AsyncOpts.cur_opt := stm_options;
 
@@ -2670,7 +2720,7 @@ let new_doc { doc_type ; ml_load_path; vo_load_path; require_libs; stm_options }
   end;
 
   (* Import initial libraries. *)
-  List.iter require_file require_libs;
+  List.iter handle_injection injections;
 
   (* We record the state at this point! *)
   State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial;
diff --git a/stm/stm.mli b/stm/stm.mli
index 2c27d63b82..9780c96512 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -52,6 +52,20 @@ type stm_doc_type =
   | VioDoc      of string       (* file path *)
   | Interactive of interactive_top    (* module path *)
 
+type option_command = OptionSet of string option | OptionUnset
+
+type injection_command =
+  | OptionInjection of (Goptions.option_name * option_command)
+  (** Set flags or options before the initial state is ready. *)
+  | RequireInjection of (string * string option * bool option)
+  (** Require libraries before the initial state is
+     ready. Parameters follow [Library], that is to say,
+     [lib,prefix,import_export] means require library [lib] from
+     optional [prefix] and [import_export] if [Some false/Some true]
+     is used.  *)
+  (* -load-vernac-source interleaving is not supported yet *)
+  (* | LoadInjection of (string * bool) *)
+
 (** STM initialization options: *)
 type stm_init_options =
   { doc_type : stm_doc_type
@@ -66,12 +80,9 @@ type stm_init_options =
   (** [vo] load paths for the document. Usually extracted from -R
      options / _CoqProject *)
 
-  ; require_libs : (string * string option * bool option) list
-  (** Require [require_libs] before the initial state is
-     ready. Parameters follow [Library], that is to say,
-     [lib,prefix,import_export] means require library [lib] from
-     optional [prefix] and [import_export] if [Some false/Some true]
-     is used.  *)
+  ; injections : injection_command list
+  (** Injects Require and Set/Unset commands before the initial
+     state is ready *)
 
   ; stm_options  : AsyncOpts.stm_opt
   (** Low-level STM options *)
diff --git a/test-suite/bugs/closed/bug_7903.v b/test-suite/bugs/closed/bug_7903.v
index 55c7ee99a7..18e1884ca7 100644
--- a/test-suite/bugs/closed/bug_7903.v
+++ b/test-suite/bugs/closed/bug_7903.v
@@ -1,4 +1,4 @@
 (* Slightly improving interpretation of Ltac subterms in notations *)
 
 Notation bar x f := (let z := ltac:(exact 1) in (fun x : nat => f)).
-Check bar x (x + x).
+Check fun x => bar x (x + x).
diff --git a/test-suite/bugs/closed/bug_9583.v b/test-suite/bugs/closed/bug_9583.v
new file mode 100644
index 0000000000..14232e8578
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9583.v
@@ -0,0 +1,7 @@
+(* Was causing a stack overflow before #11613 *)
+Declare Custom Entry bla.
+Notation "[ t ]" := (t) (at level 0, t custom bla at level 0).
+Notation "] t [" := (t) (in custom bla at level 0, t custom bla at level 0).
+Notation "t" := (t) (in custom bla at level 0, t constr at level 9).
+Notation "0" := (0) (in custom bla at level 0).
+Check fun x => [ ] x [ ].
diff --git a/test-suite/bugs/closed/bug_9679.v b/test-suite/bugs/closed/bug_9679.v
new file mode 100644
index 0000000000..24e69d23f9
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9679.v
@@ -0,0 +1,6 @@
+(* Was raising an anomaly *)
+Notation "'[#' ] f '|' x .. z '=n>' b" :=
+  (fun x => .. (fun z => f b) ..)
+    (at level 201, x binder, z binder,
+     format "'[  ' [# ] '[' f  | ']'  x  ..  z  =n>  '[' b ']' ']'"
+    ).
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index f48eaac4c9..9cb019ca56 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -111,3 +111,11 @@ Warning: The format modifier is irrelevant for only parsing rules.
 File "stdin", line 280, characters 0-63:
 Warning: The only parsing modifier has no effect in Reserved Notation.
 [irrelevant-reserved-notation-only-parsing,parsing]
+fun x : nat => U (S x)
+     : nat -> nat
+V tt
+     : unit * (unit -> unit)
+fun x : nat => V x
+     : forall x : nat, nat * (?T -> ?T)
+where
+?T : [x : nat  x0 : ?T |- Type] (x0 cannot be used)
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4d4b37a8b2..b3270d4f92 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -280,3 +280,13 @@ Notation "###" := 0 (at level 0, only parsing, format "###").
 Reserved Notation "##" (at level 0, only parsing, format "##").
 
 End N.
+
+Module O.
+
+Notation U t := (match t with 0 => 0 | S t => t | _ => 0 end).
+Check fun x => U (S x).
+Notation V t := (t,fun t => t).
+Check V tt.
+Check fun x : nat => V x.
+
+End O.
diff --git a/test-suite/output/interleave_options_bad_order.out b/test-suite/output/interleave_options_bad_order.out
new file mode 100644
index 0000000000..68dbaeb7b3
--- /dev/null
+++ b/test-suite/output/interleave_options_bad_order.out
@@ -0,0 +1,4 @@
+While loading initial state:
+Warning: There is no flag or option with this name: "Extraction Optimize".
+[unknown-option,option]
+Extraction Optimize is on
diff --git a/test-suite/output/interleave_options_bad_order.v b/test-suite/output/interleave_options_bad_order.v
new file mode 100644
index 0000000000..9a70674b02
--- /dev/null
+++ b/test-suite/output/interleave_options_bad_order.v
@@ -0,0 +1,3 @@
+(* coq-prog-args: ("-unset" "Extraction Optimize" "-ri" "Extraction") *)
+
+Test Extraction Optimize.
diff --git a/test-suite/output/interleave_options_correct_order.out b/test-suite/output/interleave_options_correct_order.out
new file mode 100644
index 0000000000..76bb2016eb
--- /dev/null
+++ b/test-suite/output/interleave_options_correct_order.out
@@ -0,0 +1 @@
+Extraction Optimize is off
diff --git a/test-suite/output/interleave_options_correct_order.v b/test-suite/output/interleave_options_correct_order.v
new file mode 100644
index 0000000000..7622d6ff52
--- /dev/null
+++ b/test-suite/output/interleave_options_correct_order.v
@@ -0,0 +1,3 @@
+(* coq-prog-args: ("-ri" "Extraction" "-unset" "Extraction Optimize") *)
+
+Test Extraction Optimize.
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index c8b8660b92..524f818523 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -92,41 +92,6 @@ let create_empty_file filename =
   let f = open_out filename in
   close_out f
 
-let interp_set_option opt v old =
-  let open Goptions in
-  let err expect =
-    let opt = String.concat " " opt in
-    let got = v in (* avoid colliding with Pp.v *)
-    CErrors.user_err
-      Pp.(str "-set: " ++ str opt ++
-          str" expects " ++ str expect ++
-          str" but got " ++ str got)
-  in
-  match old with
-  | BoolValue _ ->
-    let v = match String.trim v with
-      | "true" -> true
-      | "false" | "" -> false
-      | _ -> err "a boolean"
-    in
-    BoolValue v
-  | IntValue _ ->
-    let v = String.trim v in
-    let v = match int_of_string_opt v with
-      | Some _ as v -> v
-      | None -> if v = "" then None else err "an int"
-    in
-    IntValue v
-  | StringValue _ -> StringValue v
-  | StringOptValue _ -> StringOptValue (Some v)
-
-let set_option = let open Goptions in function
-  | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt
-  | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true
-  | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v
-
-let set_options = List.iter set_option
-
 (* Compile a vernac file *)
 let compile opts copts ~echo ~f_in ~f_out =
   let open Vernac.State in
@@ -140,7 +105,7 @@ let compile opts copts ~echo ~f_in ~f_out =
                     ++ str ".")
   in
   let ml_load_path, vo_load_path = build_load_path opts in
-  let require_libs = require_libs opts in
+  let injections = injection_commands opts in
   let stm_options = opts.config.stm_flags in
   let output_native_objects = match opts.config.native_compiler with
     | NativeOff -> false | NativeOn {ondemand} -> not ondemand
@@ -165,11 +130,10 @@ let compile opts copts ~echo ~f_in ~f_out =
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
           Stm.{ doc_type = VoDoc long_f_dot_out; ml_load_path;
-                vo_load_path; require_libs; stm_options;
+                vo_load_path; injections; stm_options;
               } in
       let state = { doc; sid; proof = None; time = opts.config.time } in
       let state = load_init_vernaculars opts ~state in
-      set_options opts.config.set_options;
       let ldir = Stm.get_ldir ~doc:state.doc in
       Aux_file.(start_aux_file
         ~aux_file:(aux_file_name_for long_f_dot_out)
@@ -218,12 +182,11 @@ let compile opts copts ~echo ~f_in ~f_out =
       let doc, sid = Topfmt.(in_phase ~phase:LoadingPrelude)
           Stm.new_doc
           Stm.{ doc_type = VioDoc long_f_dot_out; ml_load_path;
-                vo_load_path; require_libs; stm_options;
+                vo_load_path; injections; stm_options;
               } in
 
       let state = { doc; sid; proof = None; time = opts.config.time } in
       let state = load_init_vernaculars opts ~state in
-      set_options opts.config.set_options;
       let ldir = Stm.get_ldir ~doc:state.doc in
       let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_in in
       let doc = Stm.finish ~doc:state.doc in
diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli
index eb66dbaafc..8c154488d0 100644
--- a/toplevel/ccompile.mli
+++ b/toplevel/ccompile.mli
@@ -17,5 +17,3 @@ val compile_files : Coqargs.t -> Coqcargs.t -> unit
 
 (** [do_vio opts] process [.vio] files in [opts] *)
 val do_vio : Coqargs.t -> Coqcargs.t -> unit
-
-val set_options : (Goptions.option_name * Coqargs.option_command) list -> unit
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 17435c051e..c7ad5edb1f 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -38,8 +38,6 @@ type color = [`ON | `AUTO | `EMACS | `OFF]
 
 type native_compiler = NativeOff | NativeOn of { ondemand : bool }
 
-type option_command = OptionSet of string option | OptionUnset
-
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter    : bool;
@@ -59,7 +57,6 @@ type coqargs_config = {
   debug       : bool;
   time        : bool;
   print_emacs : bool;
-  set_options : (Goptions.option_name * option_command) list;
 }
 
 type coqargs_pre = {
@@ -69,10 +66,9 @@ type coqargs_pre = {
 
   ml_includes : string list;
   vo_includes : Loadpath.vo_path list;
-  vo_requires : (string * string option * bool option) list;
-  (* None = No Import; Some false = Import; Some true = Export *)
 
   load_vernacular_list : (string * bool) list;
+  injections  : Stm.injection_command list;
 
   inputstate  : string option;
 }
@@ -124,7 +120,6 @@ let default_config = {
   debug        = false;
   time         = false;
   print_emacs  = false;
-  set_options  = [];
 
   (* Quiet / verbosity options should be here *)
 }
@@ -135,8 +130,8 @@ let default_pre = {
   load_rcfile  = true;
   ml_includes  = [];
   vo_includes  = [];
-  vo_requires  = [];
   load_vernacular_list = [];
+  injections   = [];
   inputstate   = None;
 }
 
@@ -167,13 +162,13 @@ let add_vo_include opts unix_path coq_path implicit =
         unix_path; coq_path; has_ml = false; implicit; recursive = true } :: opts.pre.vo_includes }}
 
 let add_vo_require opts d p export =
-  { opts with pre = { opts.pre with vo_requires = (d, p, export) :: opts.pre.vo_requires }}
+  { opts with pre = { opts.pre with injections = Stm.RequireInjection (d, p, export) :: opts.pre.injections }}
 
 let add_load_vernacular opts verb s =
-  { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }}
+    { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }}
 
 let add_set_option opts opt_name value =
-  { opts with config = { opts.config with set_options = (opt_name, value) :: opts.config.set_options }}
+  { opts with pre = { opts.pre with injections = Stm.OptionInjection (opt_name, value) :: opts.pre.injections }}
 
 (** Options for proof general *)
 let set_emacs opts =
@@ -486,10 +481,10 @@ let parse_args ~help ~init arglist : t * string list =
 
     | "-set" ->
       let opt, v = parse_option_set @@ next() in
-      add_set_option oval opt (OptionSet v)
+      add_set_option oval opt (Stm.OptionSet v)
 
     | "-unset" ->
-      add_set_option oval (to_opt_key @@ next ()) OptionUnset
+      add_set_option oval (to_opt_key @@ next ()) Stm.OptionUnset
 
     |"-native-output-dir" ->
       let native_output_dir = next () in
@@ -513,18 +508,18 @@ let parse_args ~help ~init arglist : t * string list =
     |"-config"|"--config" -> set_query oval PrintConfig
     |"-debug" -> Coqinit.set_debug (); oval
     |"-diffs" ->
-      add_set_option oval Proof_diffs.opt_name @@ OptionSet (Some (next ()))
+      add_set_option oval Proof_diffs.opt_name @@ Stm.OptionSet (Some (next ()))
     |"-stm-debug" -> Stm.stm_debug := true; oval
     |"-emacs" -> set_emacs oval
     |"-impredicative-set" ->
       set_logic (fun o -> { o with impredicative_set = Declarations.ImpredicativeSet }) oval
     |"-allow-sprop" ->
-      add_set_option oval Vernacentries.allow_sprop_opt_name (OptionSet None)
+      add_set_option oval Vernacentries.allow_sprop_opt_name (Stm.OptionSet None)
     |"-disallow-sprop" ->
-      add_set_option oval Vernacentries.allow_sprop_opt_name OptionUnset
+      add_set_option oval Vernacentries.allow_sprop_opt_name Stm.OptionUnset
     |"-sprop-cumulative" ->
       warn_deprecated_sprop_cumul();
-      add_set_option oval Vernacentries.cumul_sprop_opt_name (OptionSet None)
+      add_set_option oval Vernacentries.cumul_sprop_opt_name (Stm.OptionSet None)
     |"-indices-matter" -> set_logic (fun o -> { o with indices_matter = true }) oval
     |"-m"|"--memory" -> { oval with post = { oval.post with memory_stat = true }}
     |"-noinit"|"-nois" -> { oval with pre = { oval.pre with load_init = false }}
@@ -564,12 +559,9 @@ let parse_args ~help ~init args =
       pre = { opts.pre with
               ml_includes = List.rev opts.pre.ml_includes
             ; vo_includes = List.rev opts.pre.vo_includes
-            ; vo_requires = List.rev opts.pre.vo_requires
             ; load_vernacular_list = List.rev opts.pre.load_vernacular_list
+            ; injections = List.rev opts.pre.injections
             }
-    ; config = { opts.config with
-                 set_options = List.rev opts.config.set_options
-               } ;
     } in
   opts, extra
 
@@ -579,8 +571,8 @@ let parse_args ~help ~init args =
 (* prelude_data == From Coq Require Import Prelude. *)
 let prelude_data = "Prelude", Some "Coq", Some false
 
-let require_libs opts =
-  if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires
+let injection_commands opts =
+  if opts.pre.load_init then Stm.RequireInjection prelude_data :: opts.pre.injections else opts.pre.injections
 
 let build_load_path opts =
   let ml_path, vo_path =
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index a51ed6766a..c8634b7847 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -14,8 +14,6 @@ val default_toplevel : Names.DirPath.t
 
 type native_compiler = NativeOff | NativeOn of { ondemand : bool }
 
-type option_command = OptionSet of string option | OptionUnset
-
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter    : bool;
@@ -35,7 +33,6 @@ type coqargs_config = {
   debug       : bool;
   time        : bool;
   print_emacs : bool;
-  set_options : (Goptions.option_name * option_command) list;
 }
 
 type coqargs_pre = {
@@ -45,10 +42,10 @@ type coqargs_pre = {
 
   ml_includes : CUnix.physical_path list;
   vo_includes : Loadpath.vo_path list;
-  vo_requires : (string * string option * bool option) list;
-  (* None = No Import; Some false = Import; Some true = Export *)
 
   load_vernacular_list : (string * bool) list;
+  injections  : Stm.injection_command list;
+
   inputstate  : string option;
 }
 
@@ -79,5 +76,5 @@ val default : t
 val parse_args : help:Usage.specific_usage -> init:t -> string list -> t * string list
 val error_wrong_arg : string -> unit
 
-val require_libs : t -> (string * string option * bool option) list
+val injection_commands : t -> Stm.injection_command list
 val build_load_path : t -> CUnix.physical_path list * Loadpath.vo_path list
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 7aad856d0a..2d450d430a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -243,13 +243,13 @@ let init_document opts =
   (* Next line allows loading .vos files when in interactive mode *)
   Flags.load_vos_libraries := true;
   let ml_load_path, vo_load_path = build_load_path opts in
-  let require_libs = require_libs opts in
+  let injections = injection_commands opts in
   let stm_options = opts.config.stm_flags in
   let open Vernac.State in
   let doc, sid =
     Stm.(new_doc
            { doc_type = Interactive opts.config.logic.toplevel_name;
-             ml_load_path; vo_load_path; require_libs; stm_options;
+             ml_load_path; vo_load_path; injections; stm_options;
            }) in
   { doc; sid; proof = None; time = opts.config.time }
 
@@ -273,7 +273,6 @@ type run_mode = Interactive | Batch
 let init_toploop opts =
   let state = init_document opts in
   let state = Ccompile.load_init_vernaculars opts ~state in
-  Ccompile.set_options opts.config.set_options;
   state
 
 let coqtop_init run_mode ~opts =
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index cc9b840bed..4242f06844 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -475,7 +475,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   let indnames = List.map (fun ind -> ind.ind_name) indl in
 
   (* In case of template polymorphism, we need to compute more constraints *)
-  let env0 = if poly then env0 else Environ.set_universes_lbound env0 Univ.Level.prop in
+  let env0 = if poly then env0 else Environ.set_universes_lbound env0 UGraph.Bound.Prop in
 
   let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl) =
     interp_params env0 udecl uparamsl paramsl
diff --git a/vernac/library.ml b/vernac/library.ml
index 85db501e84..c30331b221 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -89,6 +89,7 @@ type library_disk = {
 type summary_disk = {
   md_name : compilation_unit_name;
   md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
+  md_ocaml : string;
 }
 
 (*s Modules loaded in memory contain the following informations. They are
@@ -251,6 +252,7 @@ let intern_from_file f =
   let (univs : seg_univ option), digest_u = ObjFile.marshal_in_segment ch ~segment:"universes" in
   let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch ~segment:"opaques" in
   ObjFile.close_in ch;
+  System.check_caml_version ~caml:lsd.md_ocaml ~file:f;
   register_library_filename lsd.md_name f;
   add_opaque_table lsd.md_name (ToFetch del_opaque);
   let open Safe_typing in
@@ -401,6 +403,7 @@ let load_library_todo f =
   let tasks, _ = ObjFile.marshal_in_segment ch ~segment:"tasks" in
   let (s4 : seg_proofs), _ = ObjFile.marshal_in_segment ch ~segment:"opaques" in
   ObjFile.close_in ch;
+  System.check_caml_version ~caml:s0.md_ocaml ~file:f;
   if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
   if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
   if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
@@ -486,6 +489,7 @@ let save_library_to todo_proofs ~output_native_objects dir f otab =
     let sd = {
     md_name = dir;
     md_deps = Array.of_list (current_deps ());
+    md_ocaml = Coq_config.caml_version;
   } in
   let md = {
     md_compiled = cenv;
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 3b9c771b93..32affd562f 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1073,12 +1073,12 @@ let make_internalization_vars recvars mainvars typs =
   let extratyps = List.map (fun (x,y) -> (y,List.assoc x maintyps)) recvars in
   maintyps @ extratyps
 
-let make_interpretation_type isrec isonlybinding = function
+let make_interpretation_type isrec isonlybinding default_if_binding = function
   (* Parsed as constr list *)
   | ETConstr (_,None,_) when isrec -> NtnTypeConstrList
-  (* Parsed as constr, but interpreted as a binder: default is to parse it as an ident only *)
+  (* Parsed as constr, but interpreted as a binder *)
   | ETConstr (_,Some bk,_) -> NtnTypeBinder (NtnBinderParsedAsConstr bk)
-  | ETConstr (_,None,_) when isonlybinding -> NtnTypeBinder (NtnBinderParsedAsConstr AsIdent)
+  | ETConstr (_,None,_) when isonlybinding -> NtnTypeBinder (NtnBinderParsedAsConstr default_if_binding)
   (* Parsed as constr, interpreted as constr *)
   | ETConstr (_,None,_) -> NtnTypeConstr
   (* Others *)
@@ -1096,7 +1096,9 @@ let subentry_of_constr_prod_entry = function
   | ETConstr (InConstrEntry,_,_) -> InConstrEntrySomeLevel
   | _ -> InConstrEntrySomeLevel
 
-let make_interpretation_vars recvars allvars typs =
+let make_interpretation_vars
+  (* For binders, default is to parse only as an ident *) ?(default_if_binding=AsIdent)
+   recvars allvars typs =
   let eq_subscope (sc1, l1) (sc2, l2) =
     Option.equal String.equal sc1 sc2 &&
     List.equal String.equal l1 l2
@@ -1113,7 +1115,7 @@ let make_interpretation_vars recvars allvars typs =
   Id.Map.mapi (fun x (isonlybinding, sc) ->
     let typ = Id.List.assoc x typs in
     ((subentry_of_constr_prod_entry typ,sc),
-     make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars
+     make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding default_if_binding typ)) mainvars
 
 let check_rule_productivity l =
   if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then
@@ -1792,8 +1794,8 @@ let try_interp_name_alias = function
   | _ -> raise Not_found
 
 let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } =
-  let vars,reversibility,pat =
-    try [], APrioriReversible, NRef (try_interp_name_alias (vars,c))
+  let acvars,pat,reversibility =
+    try Id.Map.empty, NRef (try_interp_name_alias (vars,c)), APrioriReversible
     with Not_found ->
       let fold accu id = Id.Map.add id NtnInternTypeAny accu in
       let i_vars = List.fold_left fold Id.Map.empty vars in
@@ -1801,10 +1803,11 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing
         ninterp_var_type = i_vars;
         ninterp_rec_vars = Id.Map.empty;
       } in
-      let nvars, pat, reversibility = interp_notation_constr env nenv c in
-      let map id = let (_,sc) = Id.Map.find id nvars in (id, sc) in
-      List.map map vars, reversibility, pat
+      interp_notation_constr env nenv c
   in
+  let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,0))) in
+  let interp = make_interpretation_vars ~default_if_binding:AsIdentOrPattern [] acvars (List.map in_pat vars) in
+  let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in
   let onlyparsing = onlyparsing || fst (printability None false reversibility pat) in
   Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat)
 
diff --git a/vernac/record.ml b/vernac/record.ml
index 9fda98d08e..36254780cd 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -121,7 +121,7 @@ let typecheck_params_and_fields def poly pl ps records =
      any Set <= i constraint for universes that might actually be instantiated with Prop. *)
   let is_template =
     List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in
-  let env0 = if not poly && is_template then Environ.set_universes_lbound env0 Univ.Level.prop else env0 in
+  let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in
   let () =
     let error bk {CAst.loc; v=name} =