From 7ed5fc97242777655d9128ebf695d18083d5a699 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 30 Apr 2020 11:29:28 +0200
Subject: nit: don't open Persistent_cache in micromega

---
 plugins/micromega/coq_micromega.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 7e4c4ce5c6..790979354b 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -2029,8 +2029,6 @@ type provername = string * int option
   * The caching mechanism.
   *)
 
-open Persistent_cache
-
 module MakeCache (T : sig
   type prover_option
   type coeff
@@ -2054,7 +2052,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
-- 
cgit v1.2.3


From bd78f3282f76c31a7579dc667732821a9aac889c Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek
Date: Fri, 10 Apr 2020 19:02:07 +0200
Subject: Interleave commandline require/set/unset commands

---
 stm/stm.ml            | 66 ++++++++++++++++++++++++++++++++++++++++++++-------
 stm/stm.mli           | 23 +++++++++++++-----
 toplevel/ccompile.ml  | 43 +++------------------------------
 toplevel/ccompile.mli |  2 --
 toplevel/coqargs.ml   | 36 +++++++++++-----------------
 toplevel/coqargs.mli  |  9 +++----
 toplevel/coqtop.ml    |  5 ++--
 7 files changed, 97 insertions(+), 87 deletions(-)

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/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 =
-- 
cgit v1.2.3


From 684bbe55e9ee94f93486da6d2df97fcef3136d88 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 12 May 2020 14:54:41 +0200
Subject: Document the changes regarding the order of command-line options.

---
 doc/changelog/08-tools/11851-coqc-flags-fix.rst | 11 ++--
 doc/sphinx/practical-tools/coq-commands.rst     | 75 ++++++++++++++++++-------
 2 files changed, 62 insertions(+), 24 deletions(-)

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 545bba4930..ca167c8b4b 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,17 +163,44 @@ 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.
 :-compile *file.v*: Deprecated; use ``coqc`` instead. Compile file *file.v* into *file.vo*. This option
   implies -batch (exit just after argument parsing). It is available only
@@ -184,11 +211,11 @@ and ``coqtop``, unless stated otherwise:
   This option is available for ``coqc`` only; it is the counterpart of
   -compile-verbose.
 :-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
@@ -198,7 +225,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
@@ -224,17 +251,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.
-- 
cgit v1.2.3


From 4c5e40b76960f798857919bb7d500aa5d86a424d Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 12 May 2020 15:09:37 +0200
Subject: Test interleaving of command-line options.

---
 test-suite/output/interleave_options_bad_order.out     | 4 ++++
 test-suite/output/interleave_options_bad_order.v       | 3 +++
 test-suite/output/interleave_options_correct_order.out | 1 +
 test-suite/output/interleave_options_correct_order.v   | 3 +++
 4 files changed, 11 insertions(+)
 create mode 100644 test-suite/output/interleave_options_bad_order.out
 create mode 100644 test-suite/output/interleave_options_bad_order.v
 create mode 100644 test-suite/output/interleave_options_correct_order.out
 create mode 100644 test-suite/output/interleave_options_correct_order.v

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.
-- 
cgit v1.2.3


From 3e04d6c024dd03878b0b487cf823f5586d6fd397 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 3 May 2020 20:34:41 +0200
Subject: Store the OCaml version used for Coq in vo files.

---
 checker/check.ml  |  9 +++++++++
 checker/values.ml |  2 +-
 vernac/library.ml | 12 ++++++++++++
 3 files changed, 22 insertions(+), 1 deletion(-)

diff --git a/checker/check.ml b/checker/check.ml
index 31bfebc3d5..26de2db109 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 ()
@@ -289,6 +290,11 @@ let name_clash_message dir mdir f =
   pr_dirpath mdir ++ spc () ++ str "and not library" ++ spc() ++
   pr_dirpath dir
 
+let caml_version_mismatch s f =
+  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
+
 type intern_mode = Rec | Root | Dep (* Rec = standard, Root = -norec, Dep = dependency of norec *)
 
 (* Dependency graph *)
@@ -345,6 +351,9 @@ 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
+      if Coq_config.caml_version <> sd.md_ocaml then
+        user_err ~hdr:"intern_from_file"
+          (caml_version_mismatch sd.md_ocaml f);
       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/vernac/library.ml b/vernac/library.ml
index 85db501e84..2cd642c7e8 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
@@ -244,6 +245,14 @@ let mk_summary m = {
   libsum_digests = m.library_digests;
 }
 
+let check_ocaml_version num f =
+  if not (String.equal num Coq_config.caml_version) then
+  user_err Pp.(
+    str ("The file " ^ f ^ " was compiled with OCaml") ++ spc () ++
+    str num ++ spc () ++ str "while this instance of Coq was compiled with OCaml" ++
+    spc () ++ str Coq_config.caml_version
+  )
+
 let intern_from_file f =
   let ch = raw_intern_library f in
   let (lsd : seg_sum), digest_lsd = ObjFile.marshal_in_segment ch ~segment:"summary" in
@@ -251,6 +260,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;
+  check_ocaml_version lsd.md_ocaml f;
   register_library_filename lsd.md_name f;
   add_opaque_table lsd.md_name (ToFetch del_opaque);
   let open Safe_typing in
@@ -401,6 +411,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;
+  check_ocaml_version s0.md_ocaml 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 +497,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;
-- 
cgit v1.2.3


From 9e315837fded9763c3d7ca14a8aad0e7af3b4820 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 May 2020 12:55:19 +0200
Subject: Centralize the OCaml version-checking function.

We tweak the message a bit.
---
 checker/check.ml  |  9 +--------
 lib/system.ml     |  9 +++++++++
 lib/system.mli    |  2 ++
 vernac/library.ml | 12 ++----------
 4 files changed, 14 insertions(+), 18 deletions(-)

diff --git a/checker/check.ml b/checker/check.ml
index 26de2db109..6d307b3c5e 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -290,11 +290,6 @@ let name_clash_message dir mdir f =
   pr_dirpath mdir ++ spc () ++ str "and not library" ++ spc() ++
   pr_dirpath dir
 
-let caml_version_mismatch s f =
-  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
-
 type intern_mode = Rec | Root | Dep (* Rec = standard, Root = -norec, Dep = dependency of norec *)
 
 (* Dependency graph *)
@@ -351,9 +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
-      if Coq_config.caml_version <> sd.md_ocaml then
-        user_err ~hdr:"intern_from_file"
-          (caml_version_mismatch sd.md_ocaml f);
+      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/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/vernac/library.ml b/vernac/library.ml
index 2cd642c7e8..c30331b221 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -245,14 +245,6 @@ let mk_summary m = {
   libsum_digests = m.library_digests;
 }
 
-let check_ocaml_version num f =
-  if not (String.equal num Coq_config.caml_version) then
-  user_err Pp.(
-    str ("The file " ^ f ^ " was compiled with OCaml") ++ spc () ++
-    str num ++ spc () ++ str "while this instance of Coq was compiled with OCaml" ++
-    spc () ++ str Coq_config.caml_version
-  )
-
 let intern_from_file f =
   let ch = raw_intern_library f in
   let (lsd : seg_sum), digest_lsd = ObjFile.marshal_in_segment ch ~segment:"summary" in
@@ -260,7 +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;
-  check_ocaml_version lsd.md_ocaml f;
+  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
@@ -411,7 +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;
-  check_ocaml_version s0.md_ocaml f;
+  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");
-- 
cgit v1.2.3


From f71ef93aa21cd2ed4135588db3a5a3e8b42ceb39 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 May 2020 14:01:00 +0200
Subject: Make explicit that UGraph lower bounds are only of two kinds.

This makes the invariants in the code clearer, and also highlight this is
only required to implement template polymorphic inductive types.
---
 engine/uState.ml       | 14 +++++++++-----
 engine/uState.mli      |  6 +++---
 engine/univMinim.ml    |  8 ++++++--
 engine/univMinim.mli   |  2 +-
 engine/univops.mli     |  2 +-
 kernel/environ.ml      |  4 ++--
 kernel/environ.mli     |  6 +++---
 kernel/indTyping.ml    |  2 +-
 kernel/uGraph.ml       |  6 ++++++
 kernel/uGraph.mli      | 10 ++++++++--
 library/global.mli     |  2 +-
 vernac/comInductive.ml |  2 +-
 vernac/record.ml       |  2 +-
 13 files changed, 43 insertions(+), 23 deletions(-)

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/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/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/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/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} =
-- 
cgit v1.2.3


From 354cf4233194e948a4630bf180643974017dc342 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 May 2020 17:33:27 +0200
Subject: Tests for bugs #9583 (fixed by #11613) and #9679.

---
 test-suite/bugs/closed/bug_9583.v | 7 +++++++
 test-suite/bugs/closed/bug_9679.v | 6 ++++++
 2 files changed, 13 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_9583.v
 create mode 100644 test-suite/bugs/closed/bug_9679.v

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 ']' ']'"
+    ).
-- 
cgit v1.2.3


From 466e6737de8772f46f08ea8e38fda196993597c0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 23 Oct 2018 16:33:39 +0200
Subject: Extending support for mixing binders and terms in abbreviations.

---
 interp/constrintern.ml            | 11 +++--------
 interp/syntax_def.ml              | 16 +++-------------
 interp/syntax_def.mli             |  8 +++-----
 test-suite/bugs/closed/bug_7903.v |  2 +-
 test-suite/output/Notations4.out  |  8 ++++++++
 test-suite/output/Notations4.v    | 10 ++++++++++
 vernac/metasyntax.ml              | 23 +++++++++++++----------
 7 files changed, 41 insertions(+), 37 deletions(-)

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/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/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/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)
 
-- 
cgit v1.2.3


From d5a6c8a9971214c6f1f4d672fcaea846c7d2a37d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 14 Apr 2020 16:18:24 +0200
Subject: Documenting notations with both terms and binders.

Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
---
 doc/sphinx/user-extensions/syntax-extensions.rst | 46 ++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index ea5ad79a80..c5ec636d5f 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).
+
 .. _numeral-notations:
 
 Numeral notations
-- 
cgit v1.2.3


From 9e3f16880dd67bebf31bfd95f6affa5f32abb60c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 15 Apr 2020 15:45:34 +0200
Subject: Overlay elpi

---
 .../8808-herbelin-master+support-binder+term-in-abbrev.sh           | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh

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
-- 
cgit v1.2.3


From e9692bedfe275668aeaa244811e090c49f6df64d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 May 2020 22:45:53 +0200
Subject: Adding change log for #8808.

---
 .../03-notations/8808-master+support-binder+term-in-abbrev.rst        | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst

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).
-- 
cgit v1.2.3


From 2bdea3e8fd018e18f22686efdfa8deeb64e9e8e2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 14 May 2020 01:55:55 +0200
Subject: [ci] [sf] Fix SF build.

We move from the previous complex CI download setup to a much more
straightforward public mirror repository.

Thanks to Yishuai Li and Benjamin Pierce for the very quick response.

Closes #12290
---
 dev/ci/ci-basic-overlay.sh |  7 +++++++
 dev/ci/ci-sf.sh            | 23 +++++------------------
 2 files changed, 12 insertions(+), 18 deletions(-)

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 )
-- 
cgit v1.2.3