aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.bintray.json20
-rw-r--r--.travis.yml33
-rw-r--r--CHANGES121
-rw-r--r--Makefile.ide41
-rwxr-xr-xdev/build/osx/make-macos-dmg.sh14
-rw-r--r--dev/doc/changes.txt3
-rw-r--r--doc/refman/RefMan-tac.tex62
-rw-r--r--doc/refman/Universes.tex14
-rw-r--r--lib/minisys.ml4
9 files changed, 205 insertions, 107 deletions
diff --git a/.bintray.json b/.bintray.json
new file mode 100644
index 0000000000..9bae43846f
--- /dev/null
+++ b/.bintray.json
@@ -0,0 +1,20 @@
+{
+ "package": {
+ "name": "coq",
+ "repo": "coq",
+ "subject": "coq"
+ },
+
+ "version": {
+ "name": "8.7+alpha"
+ },
+
+ "files":
+ [
+ {"includePattern": "_build/(.*\\.dmg)", "uploadPattern": "$1",
+ "matrixParams": {
+ "override": 1 }
+ }
+ ],
+ "publish": true
+}
diff --git a/.travis.yml b/.travis.yml
index 9c7ad553f5..7a0e80b540 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -32,6 +32,7 @@ env:
- COMPILER="system"
- CAMLP5_VER="6.14"
- NATIVE_COMP="yes"
+ - COQ_DEST="-local"
# Main test suites
matrix:
- TEST_TARGET="test-suite" COMPILER="4.02.3+32bit"
@@ -139,11 +140,37 @@ matrix:
env:
- TEST_TARGET="test-suite"
- COMPILER="4.02.3"
+ - CAMLP5_VER="6.17"
- NATIVE_COMP="no"
+ - COQ_DEST="-local"
before_install:
- brew update
- - brew install opam
- - brew install gnu-time
+ - brew install opam gnu-time
+
+ - os: osx
+ env:
+ - TEST_TARGET=""
+ - COMPILER="4.02.3"
+ - CAMLP5_VER="6.17"
+ - NATIVE_COMP="no"
+ - COQ_DEST="-prefix ${PWD}/_install"
+ - EXTRA_CONF="-coqide opt -warn-error"
+ - EXTRA_OPAM="lablgtk-extras"
+ before_install:
+ - brew update
+ - brew install opam gnu-time gtk+ expat gtksourceview libxml2 gdk-pixbuf python3
+ - pip3 install macpack
+ before_deploy:
+ - dev/build/osx/make-macos-dmg.sh
+ deploy:
+ provider: bintray
+ user: maximedenes
+ file: .bintray.json
+ key:
+ secure: "GDRjXPNvYHJBPMJqbXsSUAAPAZeGvr+mns80eYUD47Uxvueivql5VJ9d8MwLRJOV6lzwnQ1+F65WOKsR/JARMMRuVUKg3dAa3w1j8s2Yr/gwqsLt0G4Roqp93eTFDvs2X0xzzncN31G/NcV/5suc3oXuqjIF7EUSyrtiJUpMcIfFoMHWmdcGM9az4djIKYTzczAs+8MPSfrYD1AAqx2Ezeu+xDEmtvQ0w7OyO48ArUO4K5AWCRWdzSMN0A2s1w72fiCEfMgqzphzzJfRMPzp0rTF6/4CKRbtJpnSGtvovn2TeCRVDI8Y9k61nY5w5rR5Mcdf1K9BA1wzP2L4nTBoHbur70eMdEmeM3R2e9LzFETmuUAFh7L1k6LDhx7kFqjnSLwPSVa8ALK1bJDjgv1i300NCo5divaY/mjIr9e2/AZWL3MQjdwceoVZPrpCgKfpp44XdMYB/fi/wDLORQkLIm5fQMznDeYZKGceILRTwWyjL8Yyy+bBfA++frNLF8Agknfm0gGEI9VBaF7TVYbDJrZ2lmdT68D1hagJ8g1vief7HArTgapHfLxLL2BYWmapEm284GowHDrg4hGHd1aZu+wIh10SzPp4tTGRp0scu/x4ZEr7cglKgegwy9L7ubFA7zm9E368Y6RMxYXETBGgeEVDAqVnfBHIOZVvBIEgsCw="
+ skip_cleanup: true
+ on:
+ all_branches: true
before_install:
- if [ "${TRAVIS_PULL_REQUEST}" != "false" ]; then echo "Tested commit (followed by parent commits):"; git log -1; for commit in `git log -1 --format="%P"`; do echo; git log -1 $commit; done; fi
@@ -159,7 +186,7 @@ script:
- set -e
- echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r'
-- ./configure -local -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
+- ./configure ${COQ_DEST} -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
- echo -en 'travis_fold:end:coq.config\\r'
- echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r'
diff --git a/CHANGES b/CHANGES
index c9a8418cc0..ed2f172067 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,12 +1,13 @@
-To be inserted at the proper place:
+Changes beyond 8.7
+==================
Notations
- Recursive notations with the recursive pattern repeating on the
right (e.g. "( x ; .. ; y ; z )") now supported.
-Changes beyond V8.6
-===================
+Changes from 8.6.1 to 8.7+beta
+==============================
Tactics
@@ -46,19 +47,46 @@ Tactics
- In "Tactic Notation" or "TACTIC EXTEND", entry "constr_with_bindings"
now uses type classes and rejects terms with unresolved holes, like
entry "constr" does. To get the former behavior use
- "open_constr_with_bindings" (possible source of incompatibility.
+ "open_constr_with_bindings" (possible source of incompatibility).
- New e-variants eassert, eenough, epose proof, eset, eremember, epose
which behave like the corresponding variants with no "e" but turn
unresolved implicit arguments into existential variables, on the
shelf, rather than failing.
+- Tactic injection has become more powerful (closes BZ#4890) and its
+ documentation has been updated.
+- New variants of the `first` and `solve` tacticals that do not rely
+ on parsing rules, meant to define tactic notations.
+- Added support for side effects hooks in `cbv`, `cbn` and `simpl`.
+ The side effects are provided via a plugin:
+ https://github.com/herbelin/reduction-effects/
+- It is now possible to take hint database names as parameters in a
+ Ltac definition or a Tactic Notation.
+- New option `Set Ltac Batch Debug` on top of `Set Ltac Debug` for
+ non-interactive Ltac debug output.
-Vernacular Commands
+Gallina
-- Goals context can be printed in a more compact way when "Set
- Printing Compact Contexts" is activated.
+- Now supporting all kinds of binders, including 'pat, in syntax of record fields.
+Vernacular Commands
+
+- Goals context can be printed in a more compact way when `Set
+ Printing Compact Contexts` is activated.
+- Unfocused goals can be printed with the `Set Printing Unfocused`
+ option.
+- `Print` now shows the types of let-bindings.
+- The compatibility options for printing primitive projections
+ (`Set Printing Primitive Projection Parameters` and
+ `Set Printing Primitive Projection Compatibility`) are now off by default.
+- Possibility to unset the printing of notations in a more fine grained
+ fashion than `Unset Printing Notations` is provided without any
+ user-syntax. The goal is that someone creates a plugin to experiment
+ such a user-syntax, to be later integrated in Coq when stabilized.
+- `About` now tells if a reference is a coercion.
- The deprecated `Save` vernacular and its form `Save Theorem id` to
close proofs have been removed from the syntax. Please use `Qed`.
+- `Search` now sorts results by relevance (the relevance metric is a
+ weighted sum of number of distinct symbols and size of the term).
Standard Library
@@ -68,7 +96,10 @@ Standard Library
and, consequently, choice of representatives in equivalence classes.
Various proof-theoretic characterizations of choice over setoids in
file ChoiceFacts.v.
-- The BigN, BigZ, BigZ libraries are not part anymore of Coq standard
+- New lemmas about iff and about orders on positive and Z.
+- New lemmas on powerRZ.
+- Strengthened statement of JMeq_eq_dep (closes BZ#4912).
+- The BigN, BigZ, BigZ libraries are no longer part of the Coq standard
library, they are now provided by a separate repository
https://github.com/coq/bignums
The split has been done just after the Int31 library.
@@ -81,6 +112,9 @@ Standard Library
Plugins
+- The Ssreflect plugin is now distributed with Coq. Its documentation has
+ been integrated as a chapter of the reference manual. This chapter is
+ work in progress so feedback is welcome.
- The mathematical proof language (also known as declarative mode) was removed.
- A new command Extraction TestCompile has been introduced, not meant
for the general user but instead for Coq's test-suite.
@@ -124,12 +158,75 @@ Universes
- Cumulative inductive types. see prefixes "Cumulative", "NonCumulative"
for inductive definitions and the option "Set Inductive Cumulativity"
in the reference manual.
+- New syntax `foo@{_}` to instantiate a polymorphic definition with
+ anonymous universes (can also be used with `Type`).
+
+XML Protocol and internal changes
-XML Protocol
+See dev/doc/changes.txt
+
+Many bugfixes including BZ#1859, BZ#2884, BZ#3613, BZ#3943, BZ#3994,
+BZ#4250, BZ#4709, BZ#4720, BZ#4824, BZ#4844, BZ#4911, BZ#5026, BZ#5233,
+BZ#5275, BZ#5315, BZ#5336, BZ#5360, BZ#5390, BZ#5414, BZ#5417, BZ#5420,
+BZ#5439, BZ#5449, BZ#5475, BZ#5476, BZ#5482, BZ#5501, BZ#5507, BZ#5520,
+BZ#5523, BZ#5524, BZ#5553, BZ#5577, BZ#5578, BZ#5589, BZ#5597, BZ#5598,
+BZ#5607, BZ#5618, BZ#5619, BZ#5620, BZ#5641, BZ#5648, BZ#5651, BZ#5671.
+
+Many bugfixes on OS X and Windows (now the test-suite passes on these
+platforms too).
+
+Many optimizations.
+
+Many documentation improvements.
+
+Changes from 8.6 to 8.6.1
+=========================
-- The `query` call has been modified, now it carries a mandatory
- "route_id" integer parameter, that associated the result of such
- query with its generated feedback.
+- Fix #5380: Default colors for CoqIDE are actually applied.
+- Fix plugin warnings
+- Document named evars (including Show ident)
+- Fix Bug #5574, document function scope
+- Adding a test case as requested in bug 5205.
+- Fix Bug #5568, no dup notation warnings on repeated module imports
+- Fix documentation of Typeclasses eauto :=
+- Refactor documentation of records.
+- Protecting from warnings while compiling 8.6
+- Fixing an inconsistency between configure and configure.ml
+- Add test-suite checks for coqchk with constraints
+- Fix bug #5019 (looping zify on dependent types)
+- Fix bug 5550: "typeclasses eauto with" does not work with section variables.
+- Bug 5546, qualify datatype constructors when needed in Show Match
+- Bug #5535, test for Show with -emacs
+- Fix bug #5486, don't reverse ids in tuples
+- Fixing #5522 (anomaly with free vars of pat)
+- Fix bug #5526, don't check for nonlinearity in notation if printing only
+- Fix bug #5255
+- Fix bug #3659: -time should understand multibyte encodings.
+- FIx bug #5300: Anomaly: Uncaught exception Not_found" in "Print Assumptions".
+- Fix outdated description in RefMan.
+- Repairing `Set Rewriting Schemes`
+- Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
+- Fix description of command-line arguments for Add (Rec) LoadPath
+- Fix bug #5377: @? patterns broken.
+- add XML protocol doc
+- Fix anomaly when doing [all:Check _.] during a proof.
+- Correction of bug #4306
+- Fix #5435: [Eval native_compute in] raises anomaly.
+- Instances should obey universe binders even when defined by tactics.
+- Intern names bound in match patterns
+- funind: Ignore missing info for current function
+- Do not typecheck twice the type of opaque constants.
+- show unused intro pattern warning
+- [future] Be eager when "chaining" already resolved future values.
+- Opaque side effects
+- Fix #5132: coq_makefile generates incorrect install goal
+- Run non-tactic comands without resilient_command
+- Univs: fix bug #5365, generation of u+k <= v constraints
+- make `emit' tail recursive
+- Don't require printing-only notation to be productive
+- Fix the way setoid_rewrite handles bindings.
+- Fix for bug 5244 - set printing width ignored when given enough space
+- Fix bug 4969, autoapply was not tagging shelved subgoals correctly
Changes from V8.6beta1 to V8.6
==============================
diff --git a/Makefile.ide b/Makefile.ide
index ecfe92cc5b..542d8c252d 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -55,7 +55,8 @@ IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_
GTKSHARE=$(shell pkg-config --variable=prefix gtk+-2.0)/share
GTKBIN=$(shell pkg-config --variable=prefix gtk+-2.0)/bin
GTKLIBS=$(shell pkg-config --variable=libdir gtk+-2.0)
-
+PIXBUFBIN=$(shell pkg-config --variable=prefix gdk-pixbuf-2.0)/bin
+SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-2.0)/share
###########################################################################
# CoqIde special targets
@@ -200,15 +201,14 @@ $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents
$(MKDIR) $@/coq/
$(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $@/coq/
$(MKDIR) $@/gtksourceview-2.0/{language-specs,styles}
- $(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/
- $(INSTALLLIB) "$(GTKSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/
+ $(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-2.0/language-specs/{def.lang,language2.rng} $@/gtksourceview-2.0/language-specs/
+ $(INSTALLLIB) "$(SOURCEVIEWSHARE)/"gtksourceview-2.0/styles/{styles.rng,classic.xml} $@/gtksourceview-2.0/styles/
cp -R "$(GTKSHARE)/"locale $@
- cp -R "$(GTKSHARE)/"icons $@
cp -R "$(GTKSHARE)/"themes $@
$(COQIDEAPP)/Contents/Resources/loaders: $(COQIDEAPP)/Contents
$(MKDIR) $@
- $(INSTALLLIB) $$("$(GTKBIN)/gdk-pixbuf-query-loaders" | sed -n -e '5 s!.*= \(.*\)$$!\1!p')/libpixbufloader-png.so $@
+ $(INSTALLLIB) $$("$(PIXBUFBIN)/gdk-pixbuf-query-loaders" | sed -n -e '5 s!.*= \(.*\)$$!\1!p')/libpixbufloader-png.so $@
$(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents
$(MKDIR) $@
@@ -219,7 +219,7 @@ $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib
$(MKDIR) $@/xdg/coq
$(INSTALLLIB) ide/MacOS/default_accel_map $@/xdg/coq/coqide.keys
$(MKDIR) $@/gtk-2.0
- { "$(GTKBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\
+ { "$(PIXBUFBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\
sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \
> $@/gtk-2.0/gdk-pixbuf.loaders
{ "$(GTKBIN)/gtk-query-immodules-2.0" $@/../immodules/*.so |\
@@ -231,32 +231,11 @@ $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib
$(COQIDEAPP)/Contents/Resources/lib: $(COQIDEAPP)/Contents/Resources/immodules $(COQIDEAPP)/Contents/Resources/loaders $(COQIDEAPP)/Contents $(COQIDEINAPP)
$(MKDIR) $@
- $(INSTALLLIB) $(GTKLIBS)/charset.alias $@/
- $(MKDIR) $@/pango/1.8.0/modules
- $(INSTALLLIB) "$(GTKLIBS)/pango/1.8.0/modules/"*.so $@/pango/1.8.0/modules/
- { "$(GTKBIN)/pango-querymodules" $@/pango/1.8.0/modules/*.so |\
- sed -e "s!/.*\(/pango/1.8.0/modules/.*.so\)!@executable_path/../Resources/lib\1!"; } \
- > $@/pango/1.8.0/modules.cache
-
- for i in $$(otool -L $(COQIDEINAPP) |sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
- do cp $$i $@/; \
- ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$i) $(GTKLIBS) $@; \
- done
- for i in $@/../loaders/*.so $@/../immodules/*.so $@/pango/1.8.0/modules/*.so; \
- do \
- for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
- do cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \
- ide/MacOS/relatify_with-respect-to_.sh $$i $(GTKLIBS) $@; \
- done
- EXTRAWORK=1; \
- while [ $${EXTRAWORK} -eq 1 ]; \
- do EXTRAWORK=0; \
- for i in $@/*.dylib; \
- do for j in $$(otool -L $$i | sed -n -e "\@$(GTKLIBS)@ s/[^/]*\(\/[^ ]*\) .*$$/\1/p"); \
- do EXTRAWORK=1; cp $$j $@/; ide/MacOS/relatify_with-respect-to_.sh $@/$$(basename $$j) $(GTKLIBS) $@; done; \
- done; \
+ macpack -d ../Resources/lib $(COQIDEINAPP)
+ for i in $@/../loaders/*.so $@/../immodules/*.so; \
+ do \
+ macpack -d ../lib $$i; \
done
- ide/MacOS/relatify_with-respect-to_.sh $(COQIDEINAPP) $(GTKLIBS) $@
$(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP)/Contents/Resources/share
$(INSTALLLIB) ide/MacOS/*.icns $@
diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh
index b43ada9076..cbe2a5186f 100755
--- a/dev/build/osx/make-macos-dmg.sh
+++ b/dev/build/osx/make-macos-dmg.sh
@@ -4,19 +4,13 @@
set -e
# Configuration setup
-eval `opam config env`
-make distclean
OUTDIR=$PWD/_install
DMGDIR=$PWD/_dmg
-./configure -debug -prefix $OUTDIR -native-compiler no
VERSION=$(sed -n -e '/^let coq_version/ s/^[^"]*"\([^"]*\)"$/\1/p' configure.ml)
APP=bin/CoqIDE_${VERSION}.app
# Create a .app file with CoqIDE
-~/.local/bin/jhbuild run make -j -l2 $APP
-
-# Build Coq and run test-suite
-make && make check
+make -j $NJOBS -l2 $APP
# Add Coq to the .app file
make OLDROOT=$OUTDIR COQINSTALLPREFIX=$APP/Contents/Resources/ install-coq install-ide-toploop
@@ -29,7 +23,9 @@ mkdir -p $DMGDIR
ln -sf /Applications $DMGDIR/Applications
cp -r $APP $DMGDIR
+mkdir -p _build
+
# Temporary countermeasure to hdiutil error 5341
-head -c9703424 /dev/urandom > $DMGDIR/.padding
+# head -c9703424 /dev/urandom > $DMGDIR/.padding
-hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO CoqIDE_$VERSION.dmg
+hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO _build/CoqIDE_$VERSION.dmg
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index a48c491d33..0f1a28028c 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -188,6 +188,9 @@ In Coqlib / reference location:
- The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase
was very specific. Use tclPROGRESS instead.
+- New (internal) tactical `tclINDEPENDENTL` that combined with enter_one allows
+ to iterate a non-unit tactic on all goals and access their returned values.
+
- The unsafe flag of the Refine.refine function and its variants has been
renamed and dualized into typecheck and has been made mandatory.
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b13ae9b7b3..b3b0df5c8a 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4671,50 +4671,15 @@ congruence.
\end{ErrMsgs}
+\section{Checking properties of terms}
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-\section{Everything after this point has yet to be sorted}
-
+Each of the following tactics acts as the identity if the check succeeds, and results in an error otherwise.
\subsection{\tt constr\_eq \term$_1$ \term$_2$}
\tacindex{constr\_eq}
\label{constreq}
-This tactic applies to any goal. It checks whether its arguments are
-equal modulo alpha conversion and casts.
+This tactic checks whether its arguments are equal modulo alpha conversion and casts.
\ErrMsg \errindex{Not equal}
@@ -4722,8 +4687,8 @@ equal modulo alpha conversion and casts.
\tacindex{unify}
\label{unify}
-This tactic applies to any goal. It checks whether its arguments are
-unifiable, potentially instantiating existential variables.
+This tactic checks whether its arguments are unifiable, potentially
+instantiating existential variables.
\ErrMsg \errindex{Not unifiable}
@@ -4738,9 +4703,9 @@ unifiable, potentially instantiating existential variables.
\tacindex{is\_evar}
\label{isevar}
-This tactic applies to any goal. It checks whether its argument is an
-existential variable. Existential variables are uninstantiated
-variables generated by e.g. {\tt eapply} (see Section~\ref{apply}).
+This tactic checks whether its argument is a current existential
+variable. Existential variables are uninstantiated variables generated
+by {\tt eapply} (see Section~\ref{apply}) and some other tactics.
\ErrMsg \errindex{Not an evar}
@@ -4748,10 +4713,9 @@ variables generated by e.g. {\tt eapply} (see Section~\ref{apply}).
\tacindex{has\_evar}
\label{hasevar}
-This tactic applies to any goal. It checks whether its argument has an
-existential variable as a subterm. Unlike {\tt context} patterns
-combined with {\tt is\_evar}, this tactic scans all subterms,
-including those under binders.
+This tactic checks whether its argument has an existential variable as
+a subterm. Unlike {\tt context} patterns combined with {\tt is\_evar},
+this tactic scans all subterms, including those under binders.
\ErrMsg \errindex{No evars}
@@ -4759,8 +4723,8 @@ including those under binders.
\tacindex{is\_var}
\label{isvar}
-This tactic applies to any goal. It checks whether its argument is a
-variable or hypothesis in the current goal context or in the opened sections.
+This tactic checks whether its argument is a variable or hypothesis in the
+current goal context or in the opened sections.
\ErrMsg \errindex{Not a variable or hypothesis}
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index cd36d1d320..6ea2537399 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -332,8 +332,18 @@ Universes k l.
Check (le@{k l}).
\end{coq_example}
-User-named universes are considered rigid for unification and are never
-minimized.
+User-named universes and the anonymous universe implicitly attached to
+an explicit $Type$ are considered rigid for unification and are never
+minimized. Flexible anonymous universes can be produced with an
+underscore or by omitting the annotation to a polymorphic definition.
+
+\begin{coq_example}
+ Check (fun x => x) : Type -> Type.
+ Check (fun x => x) : Type -> Type@{_}.
+
+ Check le@{k _}.
+ Check le.
+\end{coq_example}
\subsection{\tt Unset Strict Universe Declaration.
\optindex{Strict Universe Declaration}
diff --git a/lib/minisys.ml b/lib/minisys.ml
index 1ed017e489..706f0430c3 100644
--- a/lib/minisys.ml
+++ b/lib/minisys.ml
@@ -44,11 +44,13 @@ let ok_dirname f =
(* Check directory can be opened *)
let exists_dir dir =
+ (* See BZ#5391 on windows failing on a trailing (back)slash *)
let rec strip_trailing_slash dir =
let len = String.length dir in
if len > 0 && (dir.[len-1] = '/' || dir.[len-1] = '\\')
then strip_trailing_slash (String.sub dir 0 (len-1)) else dir in
- try Sys.is_directory (strip_trailing_slash dir) with Sys_error _ -> false
+ let dir = if Sys.os_type = "Win32" then strip_trailing_slash dir else dir in
+ try Sys.is_directory dir with Sys_error _ -> false
let apply_subdir f path name =
(* we avoid all files and subdirs starting by '.' (e.g. .svn) *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 13:07:14 +0000