aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* Merge PR #6167: Fixing factorization of recursive notations with an atomic ↵Gravatar Maxime Dénès2017-11-23
|\ | | | | | | separator
* \ Merge PR #6203: Fix universe polymorphic Program obligations.Gravatar Maxime Dénès2017-11-23
|\ \
* \ \ Merge PR #6123: Nix fileGravatar Maxime Dénès2017-11-23
|\ \ \
* \ \ \ 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 #6178: Have the coq_makefile timing test-suite print moreGravatar Maxime Dénès2017-11-21
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6113: Extra work on ltac printing: fixing #5787, some parenthesesGravatar Maxime Dénès2017-11-21
|\ \ \ \ \ \ | |_|_|_|/ / |/| | | | |
| * | | | | Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Gravatar Hugo Herbelin2017-11-20
| | | | | | | | | | | | | | | | | | | | | | | | Was broken since 8.6.
| | | | | * Fixing factorization of recursive notations in the case of an atomic separator.Gravatar Hugo Herbelin2017-11-20
| |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This addresses a limitation found in math-comp seq.v file. See the example in test suite file success/Notations2.v. To go further and accept recursive notations with a separator made of several tokens, and assuming camlp5 unchanged, one would need to declare an auxiliary entry for this sequence of tokens and use it as an "atomic" (non-terminal) separator. See PR #6167 for details.
* | | | | 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
| |_|_|_|_|/ / |/| | | | | |
| | | | | * | Have the coq_makefile timing test-suite print moreGravatar Jason Gross2017-11-17
| |_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | This should help debug things like https://github.com/coq/coq/issues/5675#issuecomment-345324924 if they ever show up again.
* | | | | | 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 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.
* | | | | 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
|\ \ \ \ \
| | | | | * Introduce default.nix for Nix users.Gravatar Théo Zimmermann2017-11-09
| | | |_|/ | | |/| | | | | | | | | | | | | | | | | This file can be used to get in an environment ready to compile Coq (with `nix-shell`) or to compile and install Coq (with `nix-build`).
| | | | * 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
|\ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 01:54:52 +0000