aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-09-25Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ↵Maxime Dénès
inductive types)
2017-09-25Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ↵Maxime Dénès
let-ins and non-recursively uniform parameters
2017-09-25Merge PR #1079: Avoid generated names for html pages of the reference manual ↵Maxime Dénès
(bug #4742).
2017-09-25Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in ↵Maxime Dénès
4e70791).
2017-09-25Merge PR #1057: Reporting locations in error messages about notation formats.Maxime Dénès
2017-09-25Merge PR #1060: An optimization of tactic constructorMaxime Dénès
2017-09-25Merge PR #1075: Re-enable checker error messagesMaxime Dénès
2017-09-23Discharge.ml: cosmetic renaming of some variables.Hugo Herbelin
The point is to emphasize stronglier when we are talking about contexts or about arguments.
2017-09-23Fixing #5755 (discharging of inductive types not correct with let-ins).Hugo Herbelin
The number of effective parameters was used where the number of declarations in the signature of parameters should have been used.
2017-09-23Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).Hugo Herbelin
2017-09-23Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Hugo Herbelin
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".
2017-09-22Avoid generated names for html pages of the reference manual (bug #4742).Guillaume Melquiond
2017-09-22Merge PR #1055: Remove STM vernacularsMaxime Dénès
2017-09-22Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will work as ↵Maxime Dénès
expected.
2017-09-22Merge 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-22Merge PR #1071: Mark "Set Tactic Compat Context" as deprecated.Maxime Dénès
2017-09-22Merge PR #1070: Remove remaining occurrences of -just-parsing.Maxime Dénès
2017-09-22Merge PR #1064: coq_makefile: dont show errors from failed (ignored) rmdirMaxime Dénès
2017-09-22Merge PR #1063: [flags] Flag `open Flags`Maxime Dénès
2017-09-22Merge PR #1061: Fix appveyor buildMaxime Dénès
2017-09-21Fix -silent flag of coqchk after ff918e4.Maxime Dénès
2017-09-21Adapt checker to change in locations.Maxime Dénès
2017-09-21Proposing 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-21A 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-21Do 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-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-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-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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 19:00:57 +0000