aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* 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
* \ \ Merge PR #6132: Fixes #6129 (declaration of coercions made compatible with ↵Gravatar Maxime Dénès2017-11-16
|\ \ \ | | | | | | | | | | | | local definitions)
* \ \ \ Merge PR #6104: Fixing encoding in coqdoc output tests.Gravatar Maxime Dénès2017-11-16
|\ \ \ \
| | | * | 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.
* | | | Merge PR #6122: Remove dependency of test-suite on git (fix #5725).Gravatar Maxime Dénès2017-11-15
|\ \ \ \
| | | * | 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.
| | * | Fixing encoding in coqdoc output tests.Gravatar Hugo Herbelin2017-11-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The file links.v is using utf-8 characters so this is needed at least to test this file. For the other files, it is not completely without effect since it makes that symbols like => and forall are respectively displayed ⇒ and ∀. Maybe tests with iso-8859-1 or test without a charset option should be kept.
* | | | Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac.Gravatar Maxime Dénès2017-11-13
|\ \ \ \
| | | | * Fixing a remaining "coqdoc" problem with bug #5762 and pr #1120.Gravatar Hugo Herbelin2017-11-08
| | | |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | PR #1120 was still buggy for the following reasons: variables in the lhs of the notation were linked in the glob file while they have nowhere to link to (the binder is the notation string) [I thought the change I commited in links.html.out was actually improving but it was an overlook, sorry.]
| | * / Remove dependency of test-suite on git (fix #5725).Gravatar Théo Zimmermann2017-11-08
| |/ / |/| | | | | | | | | | | | | | | | | The two lines that this commit remove are spurious as a `git clean -dfx || true` is already performed in `test-suite/coq-makefile/template/init.sh`. While this resolves the accidental dependency on git, I am still unhappy with this call of `git clean -dfx`.
* | | Merge PR #922: New beta-iota compatibility refinementsGravatar Maxime Dénès2017-11-08
|\ \ \ | |_|/ |/| |
* | | 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 #5989: Handle ∞ in coq-makefile timing test-suiteGravatar Maxime Dénès2017-10-20
|\ \ \
* \ \ \ Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" ↵Gravatar Maxime Dénès2017-10-20
|\ \ \ \ | | | | | | | | | | | | | | | clause of an inductive definitions
| | * | | Handle ∞ in coq-makefile timing test-suiteGravatar Jason Gross2017-10-19
| | | | | | | | | | | | | | | | | | | | This should (hopefully) fix #5675.
* | | | | Moving bug numbers to BZ# format in the test-suite.Gravatar Théo Zimmermann2017-10-19
| |/ / / |/| | | | | | | | | | | | | | | Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers.
* | | | 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.
* | | | Use a nice printer for constant names in Suggest Proof Using.Gravatar Gaëtan Gilbert2017-10-10
| | | |
* | | | Take Suggest Proof Using outside the kernel.Gravatar Gaëtan Gilbert2017-10-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Also add an output test for Suggest Proof Using. This changes the .aux output: instead of getting a key >context_used "$hyps;$suggest" where $hyps is a list of the used hypotheses and $suggest is the ;-separated suggestions (or the empty string if Suggest Proof Using is unset), there is a key >context_used "$hyps" and if Suggest Proof Using is set also a key >suggest_proof_using "$suggest" For instance instead of 112 116 context_used "B A;A B;All" we get 112 116 context_used "B A" 112 116 suggest_proof_using "A B;All"
* | | | Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Gravatar Maxime Dénès2017-10-10
|\ \ \ \
* \ \ \ \ Merge PR #1126: [ltac] Warning for deprecated `Add Setoid` and `Add ↵Gravatar Maxime Dénès2017-10-09
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | Morphism` forms.
* \ \ \ \ \ Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for ↵Gravatar Maxime Dénès2017-10-09
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | | | | | | | | printing-ony Notations
* | | | | | 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)
| | | | | * | | | [ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.Gravatar Emilio Jesus Gallego Arias2017-10-05
| |_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The manual has long stated that these forms are deprecated. We add a warning for them, as indeed `Add Morphism` is an "proof evil" [*] command, and we may want to remove it in the future. We've also fixed the stdlib not to emit the warning. [*] https://ncatlab.org/nlab/show/principle+of+equivalence
| | | | | * | | romega: takes advantage of context variables with bodyGravatar Pierre Letouzey2017-10-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When a context variable x is of the form "x := body : Z", romega is now made aware of this body. Technically, we reify an equation x = body, and push a corresponding (eq_refl x) as argument of the final do_omega. See also the previous commit adding this same feature to omega (fixing bug 142).
| | | | | * | | 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 #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 ↵Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | to escape non-UTF-8 file names)
* \ \ \ \ \ \ \ Merge PR #1107: Add coqwc tests to test suiteGravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #1102: On the detection of evars which "advanced" (and a fix to ↵Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | BZ#5757)
* \ \ \ \ \ \ \ \ \ Merge PR #1101: Fixing an old proof engine bug in collecting evars with ↵Gravatar Maxime Dénès2017-10-05
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | cleared context.
| | | | | * | | | | | 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
| | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-13 00:47:30 +0000