Merge PR #10811: Allow SProp default on

Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: ppedrot

8 files changed, 36 insertions, 23 deletions

diff --git a/Makefile.build b/Makefile.build
index 139da65f07..35f5e26272 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -203,7 +203,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 # the output format of the unix command time. For instance:
 #   TIME="%C (%U user, %S sys, %e total, %M maxres)"
 
-COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS) -allow-sprop
+COQOPTS=$(NATIVECOMPUTE) $(COQWARNERROR) $(COQUSERFLAGS)
 # Beware this depends on the makefile being in a particular dir, we
 # should pass an absolute path here but windows is tricky
 # c.f. https://github.com/coq/coq/pull/9560
diff --git a/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh b/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh
new file mode 100644
index 0000000000..d7af6b7a36
--- /dev/null
+++ b/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "10811" ] || [ "$CI_BRANCH" = "sprop-default-on" ]; then
+
+    elpi_CI_REF=sprop-default-on
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+    coq_dpdgraph_CI_REF=sprop-default-on
+    coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph
+
+fi
diff --git a/doc/changelog/01-kernel/10811-sprop-default-on.rst b/doc/changelog/01-kernel/10811-sprop-default-on.rst
new file mode 100644
index 0000000000..349c44c205
--- /dev/null
+++ b/doc/changelog/01-kernel/10811-sprop-default-on.rst
@@ -0,0 +1,3 @@
+- Using ``SProp`` is now allowed by default, without needing to pass
+  ``-allow-sprop`` or use :flag:`Allow StrictProp` (`#10811
+  <https://github.com/coq/coq/pull/10811>`_, by Gaëtan Gilbert).
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index 8935ba27e3..9a9ec78edc 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -9,15 +9,16 @@ SProp (proof irrelevant propositions)
 
 This section describes the extension of |Coq| with definitionally
 proof irrelevant propositions (types in the sort :math:`\SProp`, also
-known as strict propositions). To use :math:`\SProp` you must pass
-``-allow-sprop`` to the |Coq| program or use :flag:`Allow StrictProp`.
+known as strict propositions). Using :math:`\SProp` may be prevented
+by passing ``-disallow-sprop`` to the |Coq| program or using
+:flag:`Allow StrictProp`.
 
 .. flag:: Allow StrictProp
    :name: Allow StrictProp
 
    Allows using :math:`\SProp` when set and forbids it when unset. The
    initial value depends on whether you used the command line
-   ``-allow-sprop``.
+   ``-disallow-sprop`` and ``-allow-sprop``.
 
 .. exn:: SProp not allowed, you need to Set Allow StrictProp or to use the -allow-sprop command-line-flag.
    :undocumented:
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index d13ea707bb..d48d8b900f 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -38,10 +38,10 @@ Argument scopes are [type_scope _]
 bar@{u} = nat
      : Wrap@{u} Set
 (* u |= Set < u *)
-foo@{u UnivBinders.17 v} = 
-Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,UnivBinders.17+1,v+1)}
-(* u UnivBinders.17 v |=  *)
+foo@{u UnivBinders.18 v} = 
+Type@{UnivBinders.18} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,UnivBinders.18+1,v+1)}
+(* u UnivBinders.18 v |=  *)
 Type@{i} -> Type@{j}
      : Type@{max(i+1,j+1)}
 (* {j i} |=  *)
@@ -68,19 +68,19 @@ mono
 The command has indeed failed with message:
 Universe u already exists.
 bobmorane = 
-let tt := Type@{UnivBinders.33} in
-let ff := Type@{UnivBinders.35} in tt -> ff
-     : Type@{max(UnivBinders.32,UnivBinders.34)}
+let tt := Type@{UnivBinders.34} in
+let ff := Type@{UnivBinders.36} in tt -> ff
+     : Type@{max(UnivBinders.33,UnivBinders.35)}
 The command has indeed failed with message:
 Universe u already bound.
 foo@{E M N} = 
 Type@{M} -> Type@{N} -> Type@{E}
      : Type@{max(E+1,M+1,N+1)}
 (* E M N |=  *)
-foo@{u UnivBinders.17 v} = 
-Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,UnivBinders.17+1,v+1)}
-(* u UnivBinders.17 v |=  *)
+foo@{u UnivBinders.18 v} = 
+Type@{UnivBinders.18} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,UnivBinders.18+1,v+1)}
+(* u UnivBinders.18 v |=  *)
 Inductive Empty@{E} : Type@{E} :=  
 (* E |=  *)
 Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
@@ -143,16 +143,16 @@ Applied.infunct@{u v} =
 inmod@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
-axfoo@{i UnivBinders.57 UnivBinders.58} :
-Type@{UnivBinders.57} -> Type@{i}
-(* i UnivBinders.57 UnivBinders.58 |=  *)
+axfoo@{i UnivBinders.59 UnivBinders.60} :
+Type@{UnivBinders.59} -> Type@{i}
+(* i UnivBinders.59 UnivBinders.60 |=  *)
 
 axfoo is universe polymorphic
 Argument scope is [type_scope]
 Expands to: Constant UnivBinders.axfoo
-axbar@{i UnivBinders.57 UnivBinders.58} :
-Type@{UnivBinders.58} -> Type@{i}
-(* i UnivBinders.57 UnivBinders.58 |=  *)
+axbar@{i UnivBinders.59 UnivBinders.60} :
+Type@{UnivBinders.60} -> Type@{i}
+(* i UnivBinders.59 UnivBinders.60 |=  *)
 
 axbar is universe polymorphic
 Argument scope is [type_scope]
diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index adb416e3ce..ab180769b6 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -127,7 +127,6 @@ module Options = struct
   let all_opts =
   [ { enabled = false; cmd = "-debug"; }
   ; { enabled = false; cmd = "-native_compiler"; }
-  ; { enabled = true; cmd = "-allow-sprop"; }
   ; { enabled = true; cmd = "-w +default"; }
   ]
 
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index acbd96f699..1529959cc6 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -113,7 +113,7 @@ let default_logic_config = {
   impredicative_set = Declarations.PredicativeSet;
   indices_matter = false;
   toplevel_name = Stm.TopLogical default_toplevel;
-  allow_sprop = false;
+  allow_sprop = true;
   cumulative_sprop = false;
 }
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 8555d78156..b17ca71f4c 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -79,6 +79,7 @@ let print_usage_common co command =
 \n  -dump-glob f           dump globalizations in file f (to be used by coqdoc)\
 \n  -impredicative-set     set sort Set impredicative\
 \n  -allow-sprop           allow using the proof irrelevant SProp sort\
+\n  -disallow-sprop        forbid using the proof irrelevant SProp sort\
 \n  -sprop-cumulative      make sort SProp cumulative with the rest of the hierarchy\
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
 \n  -type-in-type          disable universe consistency checking\