aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| | | | | | * | | | | | | | | Make a test for coq_makefile portable.Gravatar Pierre-Marie Pédrot2017-09-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The validity of this test depended on Makefile issueing warnings in English. We simply force the global language of the shell to be C.
* | | | | | | | | | | | | | | Merge PR #1055: Remove STM vernacularsGravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will work as ↵Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | expected.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1074: Fix BZ#5750 (recovering ability to print the hole of a ↵Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | context obtained by ltac pattern-matching)
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1071: Mark "Set Tactic Compat Context" as deprecated.Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1070: Remove remaining occurrences of -just-parsing.Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1064: coq_makefile: dont show errors from failed (ignored) rmdirGravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1063: [flags] Flag `open Flags`Gravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #1061: Fix appveyor buildGravatar Maxime Dénès2017-09-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | | | | | | | | | | * | Report missing arguments in error messageGravatar Tej Chajed2017-09-21
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Augment the "Illegal tactic application" error message with the number of extra arguments passed. Fixes BZ#5753.
| | | | | | | | | | | | | | | | | | * | | | Properly handle "coq_makefile -Q . Foo" (bug #5580).Gravatar Guillaume Melquiond2017-09-21
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | | Fix -silent flag of coqchk after ff918e4.Gravatar Maxime Dénès2017-09-21
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | | Adapt checker to change in locations.Gravatar Maxime Dénès2017-09-21
| | | | | | | | | | | | | | | | | | | | |
| | | | | | * | | | | | | | | | | | | | | Proposing meta names more distinguishable from evar names than ?M42.Gravatar Hugo Herbelin2017-09-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Using "?INTERNAL#42" with a # to emphasize a meaningless re-parsability. Tough maybe it signals too much an unelegant debugging flavor?
| | | | | | * | | | | | | | | | | | | | | A possible fix to BZ#5750 (ability to print context of ltac subterm match).Gravatar Hugo Herbelin2017-09-21
| | | | | | | |_|_|_|_|/ / / / / / / / / | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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".
| | | | | | | | | * | | | | | | | | | | [checker] Add missing Feedback printer (BZ#5587)Gravatar Emilio Jesus Gallego Arias2017-09-21
| |_|_|_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | | | | | | | | | * | | | Do not run Travis OS X packaging job on PRsGravatar Théo Zimmermann2017-09-21
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This job was useless anyway because the depoly and pre-deploy phases were not run.
| * | | | | | | | | | | | | | | | | Do not reinstall preinstalled packages under AppVeyor.Gravatar Maxime Dénès2017-09-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | | | | | | | | | | | | | | | Print Cygwin setup output rather than logging in to a file.Gravatar Maxime Dénès2017-09-21
|/ / / / / / / / / / / / / / / / /
| | | | * / / / / / / / / / / / / Mark "Set Tactic Compat Context" as deprecated.Gravatar Guillaume Melquiond2017-09-21
| |_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It was introduced in 8.5 for compatibility with a 8.4 bug.
| | | * | | | | | | | | | | | | Remove remaining occurrences of -just-parsing.Gravatar Guillaume Melquiond2017-09-21
| |_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | |
| | | | * | | | | | | | | | | In gitlab set TRAVIS_BRANCH so user overlays will work as expected.Gravatar Gaëtan Gilbert2017-09-20
| |_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | |
| | * | | | | | | | | | | | coq_makefile: dont show errors from failed (ignored) rmdirGravatar Ralf Jung2017-09-20
| |/ / / / / / / / / / / / |/| | | | | | | | | | | |
| | | | | | | | | | | | * ssr: fix canonical strucut key comparison with primproj onGravatar Enrico Tassi2017-09-20
| | | | | | | | |_|_|_|/ | | | | | | | |/| | | |
| * | | | | | / | | | | [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.
| | | | | | | | | * 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
|\ \ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 19:09:37 +0000