| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-09-22 | Merge PR #1055: Remove STM vernaculars | Maxime Dénès | |
| 2017-09-22 | Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will work as ↵ | Maxime Dénès | |
| expected. | |||
| 2017-09-22 | Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a ↵ | Maxime Dénès | |
| context obtained by ltac pattern-matching) | |||
| 2017-09-22 | Merge PR #1071: Mark "Set Tactic Compat Context" as deprecated. | Maxime Dénès | |
| 2017-09-22 | Merge PR #1070: Remove remaining occurrences of -just-parsing. | Maxime Dénès | |
| 2017-09-22 | Merge PR #1064: coq_makefile: dont show errors from failed (ignored) rmdir | Maxime Dénès | |
| 2017-09-22 | Merge PR #1063: [flags] Flag `open Flags` | Maxime Dénès | |
| 2017-09-22 | Merge PR #1061: Fix appveyor build | Maxime Dénès | |
| 2017-09-21 | Report missing arguments in error message | Tej Chajed | |
| Augment the "Illegal tactic application" error message with the number of extra arguments passed. Fixes BZ#5753. | |||
| 2017-09-21 | Properly handle "coq_makefile -Q . Foo" (bug #5580). | Guillaume Melquiond | |
| 2017-09-21 | Fix -silent flag of coqchk after ff918e4. | Maxime Dénès | |
| 2017-09-21 | Adapt checker to change in locations. | Maxime Dénès | |
| 2017-09-21 | Proposing meta names more distinguishable from evar names than ?M42. | Hugo Herbelin | |
| Using "?INTERNAL#42" with a # to emphasize a meaningless re-parsability. Tough maybe it signals too much an unelegant debugging flavor? | |||
| 2017-09-21 | A possible fix to BZ#5750 (ability to print context of ltac subterm match). | Hugo Herbelin | |
| The main fix is to use is_ident_soft. The rest of the commit is to provide something a bit more appealing than "?M-1". | |||
| 2017-09-21 | [checker] Add missing Feedback printer (BZ#5587) | Emilio Jesus Gallego Arias | |
| This fixes longstanding bug likely introduced in the first `pp` to `Feedback` migration, namely the checker didn't register a feedback printer, thus no calls to `Feedback.msg_*` were printed in the checker. This closes bug: https://coq.inria.fr/bugs/show_bug.cgi?id=5587 We fix this by adding a custom printer to the checker, this is correct as the checker owns now the full console, however a cleanup should happen in any of these two directions: - all the calls to feedback are removed, and the checker always uses its own printing mechanism. - all the calls to `Format/Printf` are removed and the checker always uses the `Feedback` mechanism. Currently, I have no opinion on this. | |||
| 2017-09-21 | Do not run Travis OS X packaging job on PRs | Théo Zimmermann | |
| This job was useless anyway because the depoly and pre-deploy phases were not run. | |||
| 2017-09-21 | Do not reinstall preinstalled packages under AppVeyor. | Maxime Dénès | |
| It seems that reinstalling gcc can leave Cygwin in a strange state, where invocations of gcc fail suddenly. I haven't figure out exactly why, but this seems to fix it. | |||
| 2017-09-21 | Print Cygwin setup output rather than logging in to a file. | Maxime Dénès | |
| 2017-09-21 | Mark "Set Tactic Compat Context" as deprecated. | Guillaume Melquiond | |
| It was introduced in 8.5 for compatibility with a 8.4 bug. | |||
| 2017-09-21 | Remove remaining occurrences of -just-parsing. | Guillaume Melquiond | |
| 2017-09-21 | Improve 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-21 | Handle multiple -w options on command line (bug #5736). | Guillaume Melquiond | |
| 2017-09-20 | In gitlab set TRAVIS_BRANCH so user overlays will work as expected. | Gaëtan Gilbert | |
| 2017-09-20 | coq_makefile: dont show errors from failed (ignored) rmdir | Ralf Jung | |
| 2017-09-20 | ssr: fix canonical strucut key comparison with primproj on | Enrico 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-19 | An 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-19 | coq_makefile: make sure compile flags for Coq and coq_makefile are in sync | Emilio 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-19 | Fixing bug #5741 (anomaly in info_trivial). | Hugo Herbelin | |
| The bug was introduced in 1559f73. | |||
| 2017-09-19 | Merge PR #1036: Unify EConstr.t equality | Maxime Dénès | |
| 2017-09-19 | Improve documentation of Status message. | Maxime Dénès | |
| 2017-09-19 | Remove STM vernaculars. | Maxime Dénès | |
| 2017-09-19 | Add XML protocol support for Wait. | Maxime Dénès | |
| 2017-09-19 | Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666). | Maxime Dénès | |
| 2017-09-19 | Merge PR #1043: Disable OSX signing for temporary artifacts. | Maxime Dénès | |
| 2017-09-19 | Document UState.universe_context. | Gaëtan Gilbert | |
| 2017-09-19 | Don'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-19 | test-suite: polymorphism | Matthieu Sozeau | |
| 2017-09-19 | proof_global: cleanup and comment close_proof | Matthieu Sozeau | |
| evd: Move constrain_variables to an operation on UState Necessary to check universe declarations correctly for deferred proofs in particular. | |||
| 2017-09-19 | Allow declaring universe binders with no constraints with @{|} | Gaëtan Gilbert | |
| 2017-09-19 | Allow 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-19 | Allow empty instance parsing @{} | Matthieu Sozeau | |
| 2017-09-19 | Merge PR #1024: Switch Travis to OSX 10.12 and Xcode 8.3.3. | Maxime Dénès | |
| 2017-09-19 | Merge PR #920: kernel: bugfix in filter_stack_domain. | Maxime Dénès | |
| 2017-09-18 | Reporting locations in error messages about notation formats. | Hugo Herbelin | |
| 2017-09-18 | Fixing two anomalies in corner cases of the syntax of notation formats. | Hugo Herbelin | |
| 2017-09-18 | Add test-suite script by Cyprien Mangin | Matthieu Sozeau | |
| 2017-09-15 | Making Ltac2 representation of data coincide with the ML-side one. | Pierre-Marie Pédrot | |
| 2017-09-15 | Merge PR #979: Fix install-doc target and other gitlab failures | Maxime Dénès | |
| 2017-09-15 | Fix CHANGES after merge of PR #1025. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |