aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-06-16Refactor documentation of records.Théo Zimmermann
This fixes bug https://coq.inria.fr/bugs/show_bug.cgi?id=4971
2017-06-02Merge PR#705: Fix bug #5019 (looping zify on dependent types)Maxime Dénès
2017-06-01Merge PR#631: Fix bug #5255Maxime Dénès
2017-06-01Fix bug #5019 (looping zify on dependent types)Jason Gross
This fixes [bug #5019](https://coq.inria.fr/bugs/show_bug.cgi?id=5019), "[zify] loops on dependent types"; before, we would see a `Z.of_nat (S ?k)` which could not be turned into `Z.succ (Z.of_nat k)`, add a hypothesis of the shape `0 <= Z.of_nat (S k)`, turn that into a hypothesis of the shape `0 <= Z.succ (Z.of_nat k)`, and loop forever on this. This may not be the "right" fix (there may be cases where `zify` should succeed where it still fails with this change), but this is a pure bugfix in the sense that the only places where it changes the behavior of `zify` are the places where, previously, `zify` looped forever.
2017-06-01Add opened bug 5019Jason Gross
2017-06-01Merge PR#710: Add test-suite checks for coqchk with constraintsMaxime Dénès
2017-05-31Merge PR#560: Reinstate fixpoint refolding in [cbn], deactivated by mistake ↵Maxime Dénès
(EDIT: for mutual fixpoints)
2017-05-31Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with ↵Maxime Dénès
section variables.
2017-05-30Add test-suite checks for coqchk with constraintsJason Gross
2017-05-30Merge PR#693: A subtle bug in tclWITHHOLES.Maxime Dénès
2017-05-30Merge PR#695: Omega: fix bug #4132Maxime Dénès
2017-05-30Fix bug 5550: "typeclasses eauto with" does not work with section variables.Théo Zimmermann
2017-05-29Omega: use "simpl" only on coefficents, not on atoms (fix #4132)Pierre Letouzey
Two issues in one: - some focused_simpl were called on the wrong locations - some focused_simpl were done on whole equations In the two cases, this could be bad if "simpl" goes too far with respect to what omega expects: later calls to "occurrence" might fail. This may happen for instance if an atom isn't a variable, but a let-in (b:=5:Z in the example).
2017-05-29Merge PR#685: Fix a bug in checkerMaxime Dénès
2017-05-29Merge PR#546: Fix for bug #4499 and other minor related bugsMaxime Dénès
2017-05-28Fix a bug in checkerAmin Timany
Universe constraints of the inductive types were not instantiated before being pushed on the environment. This commit fixes this bug.
2017-05-28Fixing a subtle bug in tclWITHHOLES.Hugo Herbelin
This fixes Théo's bug on eset.
2017-05-28Merge PR#679: Bug 5546, qualify datatype constructors when needed in Show MatchMaxime Dénès
2017-05-26Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if ↵Maxime Dénès
printing only
2017-05-26Merge PR#672: Add parsers-examples target to fiat-parsers ciMaxime Dénès
2017-05-25Bug 5546, qualify datatype constructors when neededPaul Steckler
2017-05-25Merge PR#416: Fix the way setoid_rewrite handles bindings.Maxime Dénès
2017-05-23Add parsers-examples target to fiat-parsers ciJason Gross
This tests a bit more of fiat-parsers, adding an extra ~3 minutes to the build.
2017-05-23Fix bindings handling of setoid_rewrite.Cyprien Mangin
This fixes the discrepancy between "rewrite H with (1 := x)" and "setoid_rewrite H with (1 := x)".
2017-05-20Merge PR#653: Bug #5535, test for Show with -emacsMaxime Dénès
2017-05-20Merge PR#641: Fix bug #5486, don't reverse ids in tuplesMaxime Dénès
2017-05-19add test for Show with -emacs, bug 5535Paul Steckler
2017-05-17Fixing bug #5526,allow nonlinear variables in Notation patternsPaul Steckler
2017-05-17fix swapping of ids in tuples, bug 5486Paul Steckler
2017-05-17Merge PR#635: Fixing #5522 (anomaly with free vars of pat)Maxime Dénès
2017-05-16Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).Hugo Herbelin
We seized this opportunity to factorize the code for interning `pat with more general pre-existing code. More precisely: There was already a function to compute the free variables of a pattern. Commit c6d9d4fb rewrote an approximation of it and #5222 hits cases non-treated by this function. We remove the partially-defined redundant code and use instead the existing code since intern_cases_pattern, already called, was already doing this computation. (In doing so, we discover a bug in merging names in the presence of nested "as" clauses, which we fix in previous commit. Additionally, intern_local_pattern was misleadingly overkill to simply mean a folding on Id.Set.add and we avoid the detour.
2017-05-16Fixing a bug with nested "as" clauses in "match".Hugo Herbelin
2017-05-16Merge PR#624: Switch bedrock to mit-plv baseMaxime Dénès
2017-05-15Fix #5255: [Context (x : T := y)] should mean [Let x := y].Pierre-Marie Pédrot
2017-05-14Removing a line warned unused.Hugo Herbelin
2017-05-14Removing a variable warned unused.Hugo Herbelin
2017-05-10Switch bedrock to mit-plv baseJason Gross
2017-05-10Merge PR#604: FIx bug #5300: Anomaly: Uncaught exception Not_found" in ↵Maxime Dénès
"Print Assumptions".
2017-05-09Merge PR#591: Add bmsherman/topology to the ciMaxime Dénès
2017-05-09Put .travis.yml in alphabetical orderJason Gross
2017-05-09Merge PR#609: Fix bug #3659: -time should understand multibyte encodings.Maxime Dénès
2017-05-05Fix bug #3659: -time should understand multibyte encodings.Pierre-Marie Pédrot
We assume Coq always outputs UTF-8 (is it really the case?) and cut strings after 30 UTF-8 characters instead of using the standard String function.
2017-05-03FIx bug #5300: uncaught exception in "Print Assumptions".Cyprien Mangin
2017-05-03Merge PR#603: Fix outdated description in RefMan.Maxime Dénès
2017-05-03Fix outdated description in RefMan.Théo Zimmermann
2017-05-02Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions ↵Maxime Dénès
with evars).
2017-05-02Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite filesMaxime Dénès
2017-05-02Merge PR#599: Repairing `Set Rewriting Schemes`Maxime Dénès
2017-05-02Avoiding registering files from _build_ci when not calling Makefile.ci.Hugo Herbelin
2017-05-01Add bmsherman/topology to the ciJason Gross
This development of @bmsherman tests universe polymorphism and setoid rewriting in type, and should build with v8.6 and trunk.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 15:34:53 +0000