aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| * | | | | | | | | | | | | [flags] Flag `open Flags`Gravatar Emilio Jesus Gallego Arias2017-09-20
|/ / / / / / / / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | An incoming commit is removing some toplevel-specific global flags in favor of local toplevel state; this commit flags `Flags` use so it becomes clearer in the code whether we are relying on some "global" settable status in code. A good candidate for further cleanup is the pattern: `Flags.if_verbose Feedback.msg_info`
| | | * / / / / / / / / / An optimization of tactic constructor.Gravatar Hugo Herbelin2017-09-19
| | |/ / / / / / / / / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As was questioned on Stack Overflow and discussed on Gitter, reduction of the conclusion of the goal was done up to n+1 times for a failing call to "constructor" on an inductive type of n constructors. We do it at most once. Reworking the layout of the code at the same time.
| | | | | | | | | | * | coq_makefile: make sure compile flags for Coq and coq_makefile are in syncGravatar Emilio Jesus Gallego Arias2017-09-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | E.g. -safe-string is set by configure.ml and made available to both make (via config/Makefile) and coq_makefile (via config/coq_config.ml -> lib/envars.ml -> CoqMakefile.in).
| | | | | | | | | * | | Fixing bug #5741 (anomaly in info_trivial).Gravatar Hugo Herbelin2017-09-19
| | |_|_|_|_|_|_|/ / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The bug was introduced in 1559f73.
* | | | | | | | | | | Merge PR #1036: Unify EConstr.t equalityGravatar Maxime Dénès2017-09-19
|\ \ \ \ \ \ \ \ \ \ \ | |/ / / / / / / / / / |/| | | | | | | | | |
| | * | | | | | | | | Improve documentation of Status message.Gravatar Maxime Dénès2017-09-19
| | | | | | | | | | |
| | * | | | | | | | | Remove STM vernaculars.Gravatar Maxime Dénès2017-09-19
| | | | | | | | | | |
| | * | | | | | | | | Add XML protocol support for Wait.Gravatar Maxime Dénès2017-09-19
| | | |_|/ / / / / / | | |/| | | | | | |
* | | | | | | | | | Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).Gravatar Maxime Dénès2017-09-19
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #1043: Disable OSX signing for temporary artifacts.Gravatar Maxime Dénès2017-09-19
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | * | | | | | Document UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
| | | | | | | | | | | |
| | | | | | * | | | | | Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it.
| | | | | | * | | | | | test-suite: polymorphismGravatar Matthieu Sozeau2017-09-19
| | | | | | | | | | | |
| | | | | | * | | | | | proof_global: cleanup and comment close_proofGravatar Matthieu Sozeau2017-09-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | evd: Move constrain_variables to an operation on UState Necessary to check universe declarations correctly for deferred proofs in particular.
| | | | | | * | | | | | Allow declaring universe binders with no constraints with @{|}Gravatar Gaëtan Gilbert2017-09-19
| | | | | | | | | | | |
| | | | | | * | | | | | Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Introduce a "+" modifier for universe and constraint declarations to indicate that these can be extended in the final definition/proof. By default [Definition f] is equivalent to [Definition f@{+|+}], i.e universes can be introduced and constraints as well. For [f@{}] or [f@{i j}], the constraints can be extended, no universe introduced, to maintain compatibility with existing developments. Use [f@{i j | }] to indicate that no constraint (nor universe) can be introduced. These kind of definitions could benefit from asynchronous processing. Declarations of universe binders and constraints also works for monomorphic definitions.
| | | | | | * | | | | | Allow empty instance parsing @{}Gravatar Matthieu Sozeau2017-09-19
| | | | | |/ / / / / / | | | | |/| | | | | |
* | | | | | | | | | | Merge PR #1024: Switch Travis to OSX 10.12 and Xcode 8.3.3.Gravatar Maxime Dénès2017-09-19
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #920: kernel: bugfix in filter_stack_domain.Gravatar Maxime Dénès2017-09-19
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / / / / |/| | | | | | | | | | |
| | | | | | * | | | | | Reporting locations in error messages about notation formats.Gravatar Hugo Herbelin2017-09-18
| | | | | | | | | | | |
| | | | | | * | | | | | Fixing two anomalies in corner cases of the syntax of notation formats.Gravatar Hugo Herbelin2017-09-18
| |_|_|_|_|/ / / / / / |/| | | | | | | | | |
| * | | | | | | | | | Add test-suite script by Cyprien ManginGravatar Matthieu Sozeau2017-09-18
| | | | | | | | | | |
* | | | | | | | | | | Merge PR #979: Fix install-doc target and other gitlab failuresGravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \
* | | | | | | | | | | | Fix CHANGES after merge of PR #1025.Gravatar Théo Zimmermann2017-09-15
| | | | | | | | | | | |
* | | | | | | | | | | | Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | top of the linking chain.
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1051: Using an algebraic type for distinguishing toplevel input ↵Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | from location in file
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1046: Better error messages, fix for BZ#5723Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1045: Remove unneeded fix for BZ#1715Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1042: Fixing minor typos in stm/coqideGravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1000: Update CREDITS on a best-effort basis.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1037: Parse directly to Sorts.family when appropriate.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1025: BZ#5716, read flags from project file for Compile BufferGravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | * | | | | | | | | Add debug output to brew update.Gravatar Maxime Dénès2017-09-15
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | * | | | | | | | | Switch Travis to OSX 10.12 and Xcode 8.3.3.Gravatar Maxime Dénès2017-09-15
| |_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | | Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" ↵Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Inductive-keyworded record failing even on non-dependent goal)
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #990: Prevent warning about DSTROOT being undefined.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" ↵Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | work better on them
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #962: Move dev/doc/changes to Markdown.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #955: Do not hashcons universes beforehandGravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #938: [parsing] Remove hacks for reduced Prelude.Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #811: Addressing #5434 (ltac pattern-matching refusing to match ↵Gravatar Maxime Dénès2017-09-15
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | anonymous variables)
| | | | | | | | | | | | | | | * | | | | | | | | | | | Using an algebraic type for distinguishing toplevel input from location in file.Gravatar Hugo Herbelin2017-09-14
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | * | | | | | | Avoid extra failure in the "constructor" tactic (bug #5666).Gravatar Guillaume Melquiond2017-09-14
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This changes the implementation of "constructor" from constructor 1 + ... + constructor n + fail to constructor 1 + ... + constructor n.
* | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #981: Miscellaneous fixes for notationsGravatar Maxime Dénès2017-09-13
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | | | | | | * Reference manual: A few words about the file system constraints for -Q/-R.Gravatar Hugo Herbelin2017-09-13
| | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | * Adding a test for utf8 characters in directory names.Gravatar Hugo Herbelin2017-09-13
| | | | | | | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | | | | | | | * A possible fix for BZ#5715 (escape non-utf8 win32 file names).Gravatar Hugo Herbelin2017-09-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | On Win32, Sys.readdir translates the file names to the charset of the local "code page", which may be not compatible with utf8. Warnings referring to these names can be generated. These warnings may be sent to CoqIDE. To ensure a utf8 compliant communication, we escape non-utf8 file names under win32. In the CoqIDE/Coq communication, Glib.IO.read_chars expects an utf8-encoding and raises otherwise a Glib.Error "Invalid byte sequence in conversion input". This fixes bug #5715 (Hangul characters not recognized in file names) but this does not solve the case of an operating system mounting a file system with a different coding convention than the default one, i.e. unicode using "Normalization Form Canonical Decomposition" in UTF-8 for HFS+ on MacOS X, no encoding for ext3/ext4 on Linux, (non-normalized?) UTF-16 for NTFS on Windows.
| | | | | | | | | | | | | | | | | | | | | | | | | * Complying more precisely to unicode standard.Gravatar Hugo Herbelin2017-09-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In particular, checking that it is at most 4 bytes.
| | | | | | | | | | | | | | | | | | | | | | | | | * Adding a function to escape strings with non-utf8 characters.Gravatar Hugo Herbelin2017-09-13
| | | | | | | | | | | | | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-19 03:25:58 +0000