aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2019-03-25Fix #9652: rewrite fails to detect lack of progressGaëtan Gilbert
2019-03-22Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ↵Maxime Dénès
proj Ack-by: gares Reviewed-by: mattam82 Reviewed-by: maximedenes
2019-03-14Test for SkySkimmer/coq#13Gaëtan Gilbert
(NB: this needs relevance mark fixing)
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
Note currently it's impossible to define inductives in SProp because indtypes.ml and the pretyper aren't fully plugged.
2019-03-12Merge PR #9632: Fix #9631: Instance: anomaly grounding non evar-free termEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego Ack-by: ppedrot
2019-03-12Merge PR #9596: Fix #9595: missing non-primitive-record warning with 0 field ↵Emilio Jesus Gallego Arias
record Reviewed-by: ejgallego
2019-02-26Fix #9526: Registering inductives for primitive integers doesn't check enoughMaxime Dénès
2019-02-25add testcase for primitive projectionEnrico Tassi
2019-02-25Fix #9631: Instance: anomaly grounding non evar-free termGaëtan Gilbert
2019-02-25add testcase for fixEnrico Tassi
2019-02-25add test case for "match"Enrico Tassi
2019-02-22Merge PR #9364: Apply implicit binders to Hypothesis inside sections.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-22Merge PR #9576: [library] Remove `-boot` option.Enrico Tassi
Reviewed-by: SkySkimmer Ack-by: ejgallego Reviewed-by: gares
2019-02-22Apply implicit binders to Hypothesis inside sections.Jasper Hugunin
2019-02-22Merge PR #9314: Enrich implicits for instancesGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-02-22[library] Remove `-boot` option.Emilio Jesus Gallego Arias
The `-boot` option was used to: - suppress loading of the rc_file - allow to save modules with prefix `Coq` There is no good reason disable saving of modules with `Coq` prefix by default, thus we remove this option. Fixes: #9575
2019-02-19Fix #9595: missing non-primitive-record warning with 0 field recordGaëtan Gilbert
2019-02-18Merge PR #9306: Remove Printing Primitive Projection CompatibilityMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: mattam82 Reviewed-by: maximedenes Reviewed-by: ppedrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 22:09:33 +0000