aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ↵Gravatar Maxime Dénès2017-09-25
|\ | | | | | | inductive types)
* \ Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ↵Gravatar Maxime Dénès2017-09-25
|\ \ | | | | | | | | | let-ins and non-recursively uniform parameters
* \ \ Merge PR #1079: Avoid generated names for html pages of the reference manual ↵Gravatar Maxime Dénès2017-09-25
|\ \ \ | | | | | | | | | | | | (bug #4742).
* \ \ \ Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in ↵Gravatar Maxime Dénès2017-09-25
|\ \ \ \ | | | | | | | | | | | | | | | 4e70791).
* \ \ \ \ Merge PR #1057: Reporting locations in error messages about notation formats.Gravatar Maxime Dénès2017-09-25
|\ \ \ \ \
* \ \ \ \ \ Merge PR #1060: An optimization of tactic constructorGravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #1075: Re-enable checker error messagesGravatar Maxime Dénès2017-09-25
|\ \ \ \ \ \ \
| | | | | | | * Discharge.ml: cosmetic renaming of some variables.Gravatar Hugo Herbelin2017-09-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The point is to emphasize stronglier when we are talking about contexts or about arguments.
| | | | | | | * Fixing #5755 (discharging of inductive types not correct with let-ins).Gravatar Hugo Herbelin2017-09-23
| |_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | The number of effective parameters was used where the number of declarations in the signature of parameters should have been used.
| | | | * | | Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).Gravatar Hugo Herbelin2017-09-23
| | | | | | |
| | | | | | * Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Gravatar Hugo Herbelin2017-09-23
| |_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The bug was caused by an inconsistency in different part of the code for deciding where cutting the context in between recursively uniform parameters and non-recursively uniform ones when let-ins were in the middle. We fix it by using uniformly "context_chop".
| | | | | * Avoid generated names for html pages of the reference manual (bug #4742).Gravatar Guillaume Melquiond2017-09-22
| |_|_|_|/ |/| | | |
* | | | | 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
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | * | | | 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 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
| |/ / / / / |/| | | | |
| * | | | | [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.
* | | | 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
|\ \ \ \ \
* \ \ \ \ \ 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
|\ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 19:46:12 +0000