aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
Commit message (Collapse)AuthorAge
...
* | | | | | | Prelude : no more autoload of plugins extraction and recdefGravatar Pierre Letouzey2017-06-14
| |_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The user now has to manually load them, respectively via: Require Extraction Require Import FunInd The "Import" in the case of FunInd is to ensure that the tactics functional induction and functional inversion are indeed in scope. Note that the Recdef.v file is still there as well (it contains complements used when doing Function with measures), and it also triggers a load of FunInd.v. This change is correctly documented in the refman, and the test-suite has been adapted.
| | | * | | Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
| |_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml
| | * | | Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| |/ / / |/| | |
| * | | A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let".
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \ \
| | * | Adding a test case as requested in bug 5205.Gravatar Théo Zimmermann2017-06-08
| |/ /
* | | Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a ↵Gravatar Maxime Dénès2017-06-06
|\ \ \ | | | | | | | | | | | | short econstr-cleaning of record.ml
| | | * Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Matthieu Sozeau2017-06-05
| | | | | | | | | | | | | | | | Use an explicit label ~algebraic for make_flexible_variable as well.
| | * | Merge PR#705: Fix bug #5019 (looping zify on dependent types)Gravatar Maxime Dénès2017-06-02
| | |\ \
| | * \ \ Merge PR#631: Fix bug #5255Gravatar Maxime Dénès2017-06-01
| | |\ \ \
| | | | * | Fix bug #5019 (looping zify on dependent types)Gravatar Jason Gross2017-06-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | * | Add opened bug 5019Gravatar Jason Gross2017-06-01
| | | |/ / | | |/| |
| | * | | Merge PR#699: Fix bug 5550: "typeclasses eauto with" does not work with ↵Gravatar Maxime Dénès2017-05-31
| | |\ \ \ | | | | | | | | | | | | | | | | | | section variables.
| * | | | | Fixing #5233 (missing implicit arguments for recursive records).Gravatar Hugo Herbelin2017-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was failing e.g. with Inductive foo {A : Type} : Type := { Foo : foo }. Note: the test-suite was using the bug in coindprim.v.
* | | | | | Fixing #5523 (missing support for complex constructions in recursive notations).Gravatar Hugo Herbelin2017-05-31
|/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We get rid of a complex function doing both an incremental comparison and an effect on names (Notation_ops.compare_glob_constr). For the effect on names, it was actually already done at the time of turning glob_constr to notation_constr, so it could be skipped here. For the comparison, we rely on a new incremental variant of Glob_ops.glob_eq_constr (thanks to Gaëtan for getting rid of the artificial recursivity in mk_glob_constr_eq). Seizing the opportunity to get rid of catch-all clauses in pattern-matching (as advocated by Maxime). Also make indentation closer to the one of other functions.
| | * | | Fix bug 5550: "typeclasses eauto with" does not work with section variables.Gravatar Théo Zimmermann2017-05-30
| | | | |
| * | | | Omega: use "simpl" only on coefficents, not on atoms (fix #4132)Gravatar Pierre Letouzey2017-05-29
| |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
| * | | Merge PR#634: Fix bug #5526, don't check for nonlinearity in notation if ↵Gravatar Maxime Dénès2017-05-26
| |\ \ \ | | | | | | | | | | | | | | | printing only
* | \ \ \ Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsGravatar Maxime Dénès2017-05-25
|\ \ \ \ \
* | | | | | [vernac] Remove `Save.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| | | | | | | | | | | | | | | | | | | | | | | | It has been deprecated for a while in favor of `Qed`.
| * | | | | Using type classes in the interpretation of "specialize" and "contradiction".Gravatar Hugo Herbelin2017-05-22
|/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We do that by using constr_with_bindings rather than open_constr_with_bindings (+ extra call to typeclasses in "specialize"). If my understanding is right, the only effect would be to succeed more in cases where it was failing (in inh_conv_coerce_to_gen). In particular, "specialize" and "contradiction" already have a WITHHOLES test for rejecting pending holes. Incidentally, this answers enhancement #5153.
| | * | | Fixing bug #5526,allow nonlinear variables in Notation patternsGravatar Paul Steckler2017-05-17
| | | | |
| * | | | fix swapping of ids in tuples, bug 5486Gravatar Paul Steckler2017-05-17
| | | | |
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
|\| | | |
| * | | | Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).Gravatar Hugo Herbelin2017-05-16
| |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * / Fix #5255: [Context (x : T := y)] should mean [Let x := y].Gravatar Pierre-Marie Pédrot2017-05-15
| |/ /
* | | Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 ↵Gravatar Maxime Dénès2017-05-11
|\ \ \ | | | | | | | | | | | | and 8.5/8.6 "refine"
| | * | FIx bug #5300: uncaught exception in "Print Assumptions".Gravatar Cyprien Mangin2017-05-03
| | | |
* | | | Merge PR#541: Fixing "decide equality" bug #5449Gravatar Maxime Dénès2017-05-03
|\ \ \ \
| | | * \ Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions ↵Gravatar Maxime Dénès2017-05-02
| | | |\ \ | | | | | | | | | | | | | | | | | | with evars).
| | | * \ \ Merge PR#589: remove unneeded -emacs flag in coq-prog-args in test-suite filesGravatar Maxime Dénès2017-05-02
| | | |\ \ \
| | | | * | | remove unneeded -emacs flag to coq-prog-argsGravatar Paul Steckler2017-05-01
| | | | | | |
| | | | | * | Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Gravatar Hugo Herbelin2017-05-01
| | | | |/ / | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The fix follows an invariant enforced in proofview.ml on the kind of evars that are goals or that occur in goals. One day, evar kinds will need a little cleaning... PS: This is a second attempt, completing db28e82 which was missing the case PEvar in constr_matching.ml. Indeed the attached fix to #5487 alone made #2602 failing, revealing that the real cause for #2602 was actually not fixed and that if the test for #2602 was working it was because of #5487 hiding the real problem in #2602.
* | | | | | Fix bug #5501: Universe polymorphism breaks proof involving auto.Gravatar Pierre-Marie Pédrot2017-04-30
| | | | | | | | | | | | | | | | | | | | | | | | A universe substitution was lacking as the normalized evar map was dropped.
| * | | | | Fixing "decide equality"'s bug #5449.Gravatar Hugo Herbelin2017-04-30
|/ / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The code was assuming that the terms t and u for which {t=u}+{t<>u} is proved were distinct. We refine an internal "generalize" of "u" so that it works on the two precise occurrences to abstract, even if other occurrences of u occur as subterm of t too. We also reuse the global constants found in the statement rather than reconstructing them (this seems better in case the global constants eventually get polymorphic universes?).
| | * / / Revert "Fixing #5487 (v8.5 regression on ltac-matching expressions with evars)."Gravatar Maxime Dénès2017-04-28
| | |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | One day I'll get bored of spending my nights fixing commits that were pushed without being tested, and I'll ask for removal of push rights. But for now let's pretend I haven't insisted enough: ~~~~ PLEASE TEST YOUR COMMITS BEFORE PUSHING ~~~~ Thank you!
| | * | Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).Gravatar Hugo Herbelin2017-04-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | The fix follows an invariant enforced in proofview.ml on the kind of evars that are goals or that occur in goals. One day, evar kinds will need a little cleaning...
| | * | Test for bug #5193: Uncaught exception Class_tactics.Search.ReachedLimitEx.Gravatar Pierre-Marie Pédrot2017-04-27
| | | |
| * | | Test surgical use of beta-iota in the type of variables coming fromGravatar Hugo Herbelin2017-04-27
|/ / / | | | | | | | | | pattern-matching for refine.
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-04-27
|\| |
* | | Merge PR#574: Fix bug #5476: Ltac has an inconsistent view of hypotheses.Gravatar Maxime Dénès2017-04-24
|\ \ \
* \ \ \ Merge branch v8.6 into trunkGravatar Hugo Herbelin2017-04-22
|\ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | Note: I removed what seemed to be dead code in recdef.ml (local_assum and local_def introduced with econstr branch), assuming that this is what should be done.
| | | * | Fix bug #5377: @? patterns broken.Gravatar Pierre-Marie Pédrot2017-04-20
| | |/ / | |/| |
| | * | Fix bug #5476: Ltac has an inconsistent view of hypotheses.Gravatar Pierre-Marie Pédrot2017-04-19
| |/ / |/| |
| * | Merge PR#538: Correction of bug #4306Gravatar Maxime Dénès2017-04-19
| |\ \
* | | | Add a test for bug #5321: clearbody breaks typing of goal.Gravatar Pierre-Marie Pédrot2017-04-17
| | | | | | | | | | | | | | | | The bug has been solved as a side-effect of the EConstr branch.
* | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\| | |
| * | | Fixing bug #5470 (anomaly on notations with misused "binder" type).Gravatar Hugo Herbelin2017-04-14
| | | |
| * | | Fixing bug #5469 (notation format not recognizing curly braces).Gravatar Hugo Herbelin2017-04-14
| | | |
* | | | Fix an algorithmic issue in Nsatz.Gravatar Pierre-Marie Pédrot2017-04-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We use heaps instead of continuously adding elements to an ordered list, which was quadratic in the worst case. As a byproduct, this solves bug #5359, which was due to a stack overflow on big lists.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 03:41:55 +0000