aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-09-21Print Cygwin setup output rather than logging in to a file.Maxime Dénès
2017-09-21Mark "Set Tactic Compat Context" as deprecated.Guillaume Melquiond
It was introduced in 8.5 for compatibility with a 8.4 bug.
2017-09-21Remove remaining occurrences of -just-parsing.Guillaume Melquiond
2017-09-21Improve support for "-w none" compatibility option.Guillaume Melquiond
If coqtop was started with "-w none" yet the script used "Set Warnings Append", then all the warnings were turned back to their default value. This commit turns "none" (whatever its sign) into "-all" whenever some warning status is modified afterward, in order to prevent the issue.
2017-09-21Handle multiple -w options on command line (bug #5736).Guillaume Melquiond
2017-09-20In gitlab set TRAVIS_BRANCH so user overlays will work as expected.Gaëtan Gilbert
2017-09-20coq_makefile: dont show errors from failed (ignored) rmdirRalf Jung
2017-09-20ssr: fix canonical strucut key comparison with primproj onEnrico Tassi
2017-09-20[flags] Flag `open Flags`Emilio Jesus Gallego Arias
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`
2017-09-19An optimization of tactic constructor.Hugo Herbelin
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.
2017-09-19coq_makefile: make sure compile flags for Coq and coq_makefile are in syncEmilio Jesus Gallego Arias
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).
2017-09-19Fixing bug #5741 (anomaly in info_trivial).Hugo Herbelin
The bug was introduced in 1559f73.
2017-09-19Merge PR #1036: Unify EConstr.t equalityMaxime Dénès
2017-09-19Improve documentation of Status message.Maxime Dénès
2017-09-19Remove STM vernaculars.Maxime Dénès
2017-09-19Add XML protocol support for Wait.Maxime Dénès
2017-09-19Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).Maxime Dénès
2017-09-19Merge PR #1043: Disable OSX signing for temporary artifacts.Maxime Dénès
2017-09-19Document UState.universe_context.Gaëtan Gilbert
2017-09-19Don't lose names in UState.universe_context.Gaëtan Gilbert
We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it.
2017-09-19test-suite: polymorphismMatthieu Sozeau
2017-09-19proof_global: cleanup and comment close_proofMatthieu Sozeau
evd: Move constrain_variables to an operation on UState Necessary to check universe declarations correctly for deferred proofs in particular.
2017-09-19Allow declaring universe binders with no constraints with @{|}Gaëtan Gilbert
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
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.
2017-09-19Allow empty instance parsing @{}Matthieu Sozeau
2017-09-19Merge PR #1024: Switch Travis to OSX 10.12 and Xcode 8.3.3.Maxime Dénès
2017-09-19Merge PR #920: kernel: bugfix in filter_stack_domain.Maxime Dénès
2017-09-18Reporting locations in error messages about notation formats.Hugo Herbelin
2017-09-18Fixing two anomalies in corner cases of the syntax of notation formats.Hugo Herbelin
2017-09-18Add test-suite script by Cyprien ManginMatthieu Sozeau
2017-09-15Making Ltac2 representation of data coincide with the ML-side one.Pierre-Marie Pédrot
2017-09-15Merge PR #979: Fix install-doc target and other gitlab failuresMaxime Dénès
2017-09-15Fix CHANGES after merge of PR #1025.Théo Zimmermann
2017-09-15Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ↵Maxime Dénès
top of the linking chain.
2017-09-15Merge PR #1051: Using an algebraic type for distinguishing toplevel input ↵Maxime Dénès
from location in file
2017-09-15Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.Maxime Dénès
2017-09-15Merge PR #1046: Better error messages, fix for BZ#5723Maxime Dénès
2017-09-15Merge PR #1045: Remove unneeded fix for BZ#1715Maxime Dénès
2017-09-15Merge PR #1042: Fixing minor typos in stm/coqideMaxime Dénès
2017-09-15Merge PR #1000: Update CREDITS on a best-effort basis.Maxime Dénès
2017-09-15Merge PR #1037: Parse directly to Sorts.family when appropriate.Maxime Dénès
2017-09-15Merge PR #1025: BZ#5716, read flags from project file for Compile BufferMaxime Dénès
2017-09-15Add debug output to brew update.Maxime Dénès
2017-09-15Switch Travis to OSX 10.12 and Xcode 8.3.3.Maxime Dénès
2017-09-15Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" ↵Maxime Dénès
Inductive-keyworded record failing even on non-dependent goal)
2017-09-15Merge PR #990: Prevent warning about DSTROOT being undefined.Maxime Dénès
2017-09-15Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" ↵Maxime Dénès
work better on them
2017-09-15Merge PR #962: Move dev/doc/changes to Markdown.Maxime Dénès
2017-09-15Merge PR #955: Do not hashcons universes beforehandMaxime Dénès
2017-09-15Merge PR #938: [parsing] Remove hacks for reduced Prelude.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-27 05:20:26 +0000