diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/sprop.rst | 7 | ||||
| -rw-r--r-- | test-suite/output/UnivBinders.out | 34 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 1 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 2 | ||||
| -rw-r--r-- | toplevel/usage.ml | 1 |
6 files changed, 24 insertions, 23 deletions
diff --git a/Makefile.build b/Makefile.build index f2e1ca4ea0..d13808e90b 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/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 a89fd64999..d35637d3af 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 113b1fb5d7..a6e293a2e2 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\ |