aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
Commit message (Collapse)AuthorAge
* Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ↵Gravatar Maxime Dénès2017-11-30
|\ | | | | | | #3125)
| * In injection/inversion, consider all template-polymorphic types as injectable.Gravatar Hugo Herbelin2017-11-28
| | | | | | | | | | | | | | In particular singleton inductive types are considered injectable, even in the absence of the option "Set Keep Proof Equalities". This fixes #3125 (and #4560, #6273).
* | Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gravatar Gaëtan Gilbert2017-11-28
| |
* | Fix #5347: unify declaration of axioms with and without bound univs.Gravatar Gaëtan Gilbert2017-11-25
| | | | | | | | | | | | | | | | | | Note that this makes the following syntax valid: Axiom foo@{i} bar : Type@{i}. (ie putting a universe declaration on the first axiom in the list, the declaration then holds for the whole list).
* | Make restrict_universe_context stronger.Gravatar Gaëtan Gilbert2017-11-25
|/ | | | | | This fixes BZ#5717. Also add a test and fix a changed test.
* Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRingGravatar Maxime Dénès2017-11-24
|\
* \ Merge PR #876: In omega or romega, recognizing Z and nat modulo conversionGravatar Maxime Dénès2017-11-24
|\ \
* \ \ Merge PR #6203: Fix universe polymorphic Program obligations.Gravatar Maxime Dénès2017-11-23
|\ \ \
| | * | Recognizing Z in romega up to conversion.Gravatar Hugo Herbelin2017-11-23
| | | |
| | * | Using is_conv rather than eq_constr to find `nat` or `Z` in omega.Gravatar Hugo Herbelin2017-11-23
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | Moving at the same to a passing "env sigma" style rather than passing "gl". Not that it is strictly necessary, but since we had to move functions taking only a "sigma" to functions taking also a "env", we eventually adopted the "env sigma" style. (The "gl" style would have been as good.) This answers wish #4717.
| | * Fixing a 8.7 regression of ring_simplify in ArithRing.Gravatar Hugo Herbelin2017-11-23
| |/ |/| | | | | | | With help from Guillaume (see discussion at https://github.com/coq/coq/issues/6191).
* | Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gravatar Maxime Dénès2017-11-23
|\ \
| | * Fix universe polymorphic Program obligations.Gravatar Matthieu Sozeau2017-11-22
| |/ |/| | | | | | | | | The universes of the obligations should all be non-algebraic as they might appear in instances of other obligations and instances only take non-algebraic universes as arguments.
* | Merge PR #6166: Fix regression in treating Defined as definedGravatar Maxime Dénès2017-11-20
|\ \
* \ \ Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 ↵Gravatar Maxime Dénès2017-11-20
|\ \ \ | | | | | | | | | | | | (clause "where" with implicit arguments)
* \ \ \ Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵Gravatar Maxime Dénès2017-11-20
|\ \ \ \ | | | | | | | | | | | | | | | unbound rel
| | | | * Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gravatar Gaëtan Gilbert2017-11-19
| |_|_|/ |/| | |
| | | * Fix regression in treating Defined as definedGravatar Tej Chajed2017-11-15
| | | | | | | | | | | | | | | | Fixes #6165.
| * | | Fix #5761: cbv on undefined evars under binders produces unbound relGravatar Gaëtan Gilbert2017-11-15
| | |/ | |/| | | | | | | | | | | | | | | | When an evar is undefined we need to substitute inside the evar instance. With help from @herbelin and @psteckler to identify the issue from a large test case.
* / | Fixes #6129 (declaration of coercions made compatible with local definitions).Gravatar Hugo Herbelin2017-11-14
|/ /
| * One more step in fixing #5762 ("where" clause).Gravatar Hugo Herbelin2017-11-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We improve one step further the heuristics to sort out if a variable is a notation variable or a named variable. This allows to support the following which was still failing. Reserved Notation "# x" (at level 0). Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I). We rely here on the property that a binding variable of same name as a notation variables is itself considered bound by the notation. This becomes however to be a bit tricky for sorting out if the variable has to be output to the glob file or not.
* | Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac.Gravatar Maxime Dénès2017-11-13
|\ \ | |/ |/|
* | Merge PR #6074: Refining PR#924 (insensitivity of projection heuristics to ↵Gravatar Maxime Dénès2017-11-06
|\ \ | | | | | | | | | alphabet).
* \ \ Merge PR #1139: Add a linter.Gravatar Maxime Dénès2017-11-06
|\ \ \
| | * | Refining PR#924 (insensitivity of projection heuristics to alphabet).Gravatar Hugo Herbelin2017-11-05
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | We refine the criterion for selecting a projection. Before PR#924 it was alphabetic (i.e. morally "random" up to alpha-conversion). After PR#924 it was chronological. We refine a bit more by giving priority to simple projections when they exist over projections which include an evar instantiation (and which may actually be ill-typed).
| | * Adding support for syntax "let _ := e in e'" in Ltac.Gravatar Hugo Herbelin2017-11-04
| |/ |/| | | | | Adding a file fixing #5996 and which uses this feature.
* | Merge PR #6047: A generic printer for ltac valuesGravatar Maxime Dénès2017-11-03
|\ \
* \ \ Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous ↵Gravatar Maxime Dénès2017-11-03
|\ \ \ | | | | | | | | | | | | variables).
* \ \ \ Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).Gravatar Maxime Dénès2017-11-03
|\ \ \ \
| | | * | Binding ltac printing functions to the system of generic printing.Gravatar Hugo Herbelin2017-11-02
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This concerns pr_value and message_of_value. This has a few consequences. For instance, no more ad hoc message "a term" or "a tactic", when not enough information is available for printing, one gets a generic message "a value of type foobar". But we also have more printers, satisfying e.g. request #5786.
| * | | Fixing #2881 ("change with" failing in an Ltac definition).Gravatar Hugo Herbelin2017-10-30
| | | | | | | | | | | | | | | | | | | | | | | | We fix by interpreting the pattern in "change pat with term" in strict mode by using the same interning code as for "match goal" (even if the pattern is dropped afterwards).
| | * | Fixing #5401 (printing of patterns with bound anonymous variables).Gravatar Hugo Herbelin2017-10-28
| |/ / |/| | | | | | | | This fixes also #5731, #6035, #5364.
* | | Merge PR #677: Trunk+abstracting injection flagsGravatar Maxime Dénès2017-10-27
|\ \ \ | |/ / |/| |
| * | Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281.
| | * Put newlines at the end of files.Gravatar Gaëtan Gilbert2017-10-25
| | |
* | | Move bug files to match their new GitHub ID (fixes #6001).Gravatar Théo Zimmermann2017-10-23
|/ /
* | Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" ↵Gravatar Maxime Dénès2017-10-20
|\ \ | | | | | | | | | clause of an inductive definitions
* | | Adding a test for bug BZ#5692.Gravatar Pierre-Marie Pédrot2017-10-17
| | |
* | | [stdlib] Fix warnings on deprecated `Add Setoid`Gravatar Emilio Jesus Gallego Arias2017-10-15
| | | | | | | | | | | | The test suite cases are preserved until the feature is actually removed.
* | | Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Gravatar Maxime Dénès2017-10-10
|\ \ \ | |_|/ |/| |
* | | Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type ↵Gravatar Maxime Dénès2017-10-06
|\ \ \ | | | | | | | | | | | | "_something")
* \ \ \ Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ↵Gravatar Maxime Dénès2017-10-06
|\ \ \ \ | | | | | | | | | | | | | | | inductive definition)
* \ \ \ \ Merge PR #1124: Extraction: reduce atomic eta-redexes (solves indirectly ↵Gravatar Maxime Dénès2017-10-06
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | BZ#4852)
| | | | * | Omega now aware of context variables with bodies (in type Z or nat) (fix bug ↵Gravatar Pierre Letouzey2017-10-05
| |_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 148) For compatibility, this extra feature of omega could be disabled via Unset Omega UseLocalDefs. Caveat : for now, real let-ins inside goals or hyps aren't handled, use some "cbv zeta" reduction if you want to get rid of them. And context definitions whose types aren't Z or nat are ignored, some manual "unfold" are still mandatory if expanding these definitions will help omega.
* | | | | Merge PR #1102: On the detection of evars which "advanced" (and a fix to ↵Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | BZ#5757)
| | * | | | Extraction: reduce eta-redexes whose cores are atomic (solves indirectly ↵Gravatar Pierre Letouzey2017-10-05
| |/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BZ#4852) This code simplification isn't that important, but it can trigger further simplifications elsewhere, see for instance BZ#4852. NB: normally, the extraction favors eta-expanded forms, since that's the usual way to avoid issues about '_a type variables that cannot be generalized. But the atomic eta-reductions done here shouldn't be problematic (no applications put outside of functions).
| | | * | Fixing BZ#5769 (variable of type "_something" was named after invalid "_").Gravatar Hugo Herbelin2017-10-05
| | | | |
| | * | | Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).Gravatar Hugo Herbelin2017-10-05
| | |/ /
| | | * Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Gravatar Hugo Herbelin2017-10-05
| | |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows e.g. the following to work: Reserved Notation "* a" (at level 70). Inductive P {n : nat} : nat -> Prop := c m : *m where "* m" := (P m). We seize this opportunity to make main calls to Metasyntax to depend on an arbitrary env rather than on Global.env. Incidentally, this fixes a little coqdoc bug in classifying the inductive type referred to in the "where" clause.
* | | Merge PR #1006: fix: ssrmatching and primitive projectionsGravatar Maxime Dénès2017-10-04
|\ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-04 07:05:56 +0000