aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2019-02-18Merge PR #9509: Fix #9508: Unexpected interaction between implicit arguments ↵Maxime Dénès
and primititive projections Reviewed-by: maximedenes
2019-02-17Merge PR #9528: Fix #9527: unknown evar in nonterminating [fix] error.Pierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2019-02-14Merge PR #9502: Remove nondeterministic testsThéo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48
2019-02-13more testsEnrico Tassi
2019-02-13Fix #9432: canonical structure and coercion accept universe binders.Gaëtan Gilbert
(when defining a new constant)
2019-02-11Fix #9508: Unexpected interaction between implicit arguments and primitive ↵Pierre-Marie Pédrot
projections. This was due to an involuntary capture of a variable name.
2019-02-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
2019-02-08Merge PR #9410: Make `Program` a regular attributeMatthieu Sozeau
Ack-by: SkySkimmer Reviewed-by: aspiwack Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: mattam82 Ack-by: maximedenes
2019-02-07Remove nondeterministic testsGaëtan Gilbert
Close #5982 #7388 #7483 #9497
2019-02-06Avoid eqn when generating name in induction_gen.Jasper Hugunin
Fixes #9494. Was failing with "Cannot create self-referring hypothesis" when the generated name equaled the eqn.
2019-02-05Make Program a regular attributeMaxime Dénès
We remove all calls to `Flags.is_program_mode` except one (to compute the default value of the attribute). Everything else is passed explicitely, and we remove the special logic in the interpretation loop to set/unset the flag. This is especially important since the value of the flag has an impact on proof modes, so on the separation of parsing and execution phases.
2019-02-04Enrich implicits for instancesJasper Hugunin
For compatibility, also * Adjust implicits on equiv_transitivity and equiv_symmetry, and in some closed bugs * Add overlay for HoTT setting Arguments on some instances.
2019-02-04Merge PR #9317: Restrict universes in records.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: mattam82 Reviewed-by: ppedrot
2019-02-04Merge PR #9368: Discard argument names of section variables on section closePierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2019-02-04Merge PR #9454: Fix off-by-one error in nat syntax warningsPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-02-04Merge PR #9452: [proof] optimize proof always works on incomplete proofsPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
2019-02-04Merge PR #9291: Do not take universes into account in lia reification.Frédéric Besson
Reviewed-by: fajb
2019-01-31Fix off-by-one error in nat syntax warningsJason Gross
Fixes #9453
2019-01-31add testEnrico Tassi
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
This PR deprecates the use of `coqtop` as a compiler. There is no point on having two binaries with the same purpose; after the experiment in #8690, IMHO we have a lot to gain in terms of code organization by splitting the compiler and the interactive binary. We adapt the documentation and adapt the test-suite. Note that we don't make `coqc` a true binary yet, but here we take care only of the user-facing part. The conversion of the binary will take place in #8690 and will bring code simplification, including a unified handling of arguments.
2019-01-30Restrict universes in records.Gaëtan Gilbert
Fix #8076.
2019-01-29Update update-compat.py scriptJason Gross
It now removes the outdated `CompatOldOldFlag.v` file on `--release`, and it now correctly updates `bug_9166.v` which seems to specifically be about the compat flag behavior. Additionally, it inserts an "autogenerated" notice at top of the two bug files, and makes them read-only.
2019-01-24Make `Instance` without a body always open a proof.Maxime Dénès
2019-01-24Merge PR #9377: [CS] recognize applied primitive projections as keys (fix #9375)Matthieu Sozeau
Ack-by: SkySkimmer Ack-by: gares Reviewed-by: mattam82 Ack-by: ppedrot
2019-01-23Merge PR #9270: Turn `Refine instance Mode` off by defaultPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: maximedenes Reviewed-by: ppedrot
2019-01-22Fixing #9329 (registering empty levels in the order they are recomputed).Hugo Herbelin
Was raising an anomaly 'Failure("Grammar.extend")' otherwise.
2019-01-22Turn `Refine Instance Mode` off by defaultMaxime Dénès
2019-01-22Make `Add Morphism` not rely on Refine InstanceMaxime Dénès
2019-01-22Distinguish ASTs for Instance and Declare InstanceMaxime Dénès
This makes code paths clearer (we still factorize a lot of the treatment), and we seize the opportunity to forbid anonymous `Declare Instance` which is not a documented construction, and seems to make little sense in practice.
2019-01-22[CS] recognize applied primitive projections as keys (fix #9375)Enrico Tassi
2019-01-20Discard argument names of section variables on section closeJasper Hugunin
2019-01-14Merge PR #9307: Handle local definitions in implicit arguments of InstanceMaxime Dénès
2019-01-10Remove Printing Primitive Projection CompatibilityGaëtan Gilbert
The code to generate the legacy bodies is moved to its only user in extraction. It almost seems like we could remove it (ie no special extraction code for primitive projection constants) but then we run into issues with automatic unboxing eg `Record foo := { a : nat; b : a <= 5 }.` gets extracted to `type foo = nat` and (if we remove the special code) `let a = a`.
2019-01-09Make some tests more robust by adding missing proof terminatorsMaxime Dénès
2019-01-08Fix #9272: `Unset Nested Proofs Allowed` does not capture nested `Instance` ↵Maxime Dénès
proofs. We forbid commands that may open proofs inside proofs.
2019-01-07Merge PR #9241: Fix #9240: Register for IDProp causes anomaly when non constantEnrico Tassi
2019-01-06Reworking error message for unresolved evar subterm of another evar.Hugo Herbelin
This is a reworking of 7fd28dc9: instead of using words such as "domain of", "codomain of" to refer to a position in the instance of the original evar, we simply display the instance and the name of the unresolved evar in this instance. This is both simpler and more informative. (The positional words remain useful for printing the evar_map in debugging though.) In passing, this fixes #8369 (Not_found in printing message about an unresolved subevar). Incidentally add possible breaking while printing "in environment".
2019-01-04Handle local definitions in implicit arguments of InstanceJasper Hugunin
2018-12-30Do not take universes into account in lia reification.Pierre-Marie Pédrot
This is slightly blunt, it might be the case that we get delayed constraints that cannot be solved resulting in a later universe inconsistency, but it looks highly unlikely on arithmetical statements. Alternatively we would have threaded the unification state, but this would have required a much deeper change. Fixes #9268.
2018-12-22Merge PR #9248: Fix #7904: update proofview env after ltac constr:()Pierre-Marie Pédrot
2018-12-21Fix #9240: Register for IDProp causes anomaly when non constantGaëtan Gilbert
2018-12-19Fix #7904: update proofview env after ltac constr:()Gaëtan Gilbert
(in case of side effects) Also: Fix #4781 Fix #4496
2018-12-18Fixes #9229 (Infix not robust wrt choice of variable names).Hugo Herbelin
2018-12-15Avoid explicit names in binders for automatic introsJasper Hugunin
2018-12-13Merge PR #9193: Tests for #4509, #6202 which happen to be fixed (was a lost ↵Gaëtan Gilbert
of evars in shelf)
2018-12-12Fixes #9166 (no warning on pattern variables named like a deprecated alias).Hugo Herbelin
2018-12-11Tests for #4509, #6202 which happen to be fixed (was a lost of evars in shelf).Hugo Herbelin
2018-12-05Add test for #8951.Gaëtan Gilbert
Close #8951.
2018-11-28Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a classMatthieu Sozeau
2018-11-27Fix #8364: making univ algebraic when already equal to another.Gaëtan Gilbert
When making a universe a variable we iterate through the universes we're equal to and if we find one we update the substitution accordingly. NB: The bug called make_flexible_variable on Top.15 and ~~~ {Top.15 Top.14} |= Top.11 < Top.6 Top.14 < Top.5 Top.11 = Top.15 ALGEBRAIC UNIVERSES:{Top.17 Top.16} UNDEFINED UNIVERSES:Top.17 := Top.14+1 Top.16 := Top.14+1 WEAK CONSTRAINTS: ~~~ so now we would add [Top.15 := Top.11].
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 13:06:30 +0000