aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2017-11-23Merge PR #6123: Nix fileMaxime Dénès
2017-11-23Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Maxime Dénès
2017-11-21Merge PR #6178: Have the coq_makefile timing test-suite print moreMaxime Dénès
2017-11-21Merge PR #6113: Extra work on ltac printing: fixing #5787, some parenthesesMaxime Dénès
2017-11-20Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).Hugo Herbelin
Was broken since 8.6.
2017-11-20Merge PR #6166: Fix regression in treating Defined as definedMaxime Dénès
2017-11-20Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 ↵Maxime Dénès
(clause "where" with implicit arguments)
2017-11-20Merge PR #6025: Fix #5761: cbv on undefined evars under binders produces ↵Maxime Dénès
unbound rel
2017-11-19Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gaëtan Gilbert
2017-11-17Have the coq_makefile timing test-suite print moreJason Gross
This should help debug things like https://github.com/coq/coq/issues/5675#issuecomment-345324924 if they ever show up again.
2017-11-16Merge PR #6132: Fixes #6129 (declaration of coercions made compatible with ↵Maxime Dénès
local definitions)
2017-11-16Merge PR #6104: Fixing encoding in coqdoc output tests.Maxime Dénès
2017-11-15Fix regression in treating Defined as definedTej Chajed
Fixes #6165.
2017-11-15Fix #5761: cbv on undefined evars under binders produces unbound relGaëtan Gilbert
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.
2017-11-15Merge PR #6122: Remove dependency of test-suite on git (fix #5725).Maxime Dénès
2017-11-14Fixes #6129 (declaration of coercions made compatible with local definitions).Hugo Herbelin
2017-11-14One more step in fixing #5762 ("where" clause).Hugo Herbelin
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.
2017-11-13Fixing encoding in coqdoc output tests.Hugo Herbelin
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.
2017-11-13Merge PR #6000: Adding support for syntax "let _ := e in e'" in Ltac.Maxime Dénès
2017-11-09Introduce default.nix for Nix users.Théo Zimmermann
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`).
2017-11-08Fixing a remaining "coqdoc" problem with bug #5762 and pr #1120.Hugo Herbelin
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.]
2017-11-08Remove dependency of test-suite on git (fix #5725).Théo Zimmermann
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`.
2017-11-08Merge PR #922: New beta-iota compatibility refinementsMaxime Dénès
2017-11-06Merge PR #6074: Refining PR#924 (insensitivity of projection heuristics to ↵Maxime Dénès
alphabet).
2017-11-06Merge PR #1139: Add a linter.Maxime Dénès
2017-11-05Refining PR#924 (insensitivity of projection heuristics to alphabet).Hugo Herbelin
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).
2017-11-04Adding support for syntax "let _ := e in e'" in Ltac.Hugo Herbelin
Adding a file fixing #5996 and which uses this feature.
2017-11-03Merge PR #6047: A generic printer for ltac valuesMaxime Dénès
2017-11-03Merge PR #6037: Fixing #5401 (printing of patterns with bound anonymous ↵Maxime Dénès
variables).
2017-11-03Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).Maxime Dénès
2017-11-02Binding ltac printing functions to the system of generic printing.Hugo Herbelin
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.
2017-10-30Fixing #2881 ("change with" failing in an Ltac definition).Hugo Herbelin
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).
2017-10-28Fixing #5401 (printing of patterns with bound anonymous variables).Hugo Herbelin
This fixes also #5731, #6035, #5364.
2017-10-27Merge PR #677: Trunk+abstracting injection flagsMaxime Dénès
2017-10-26Passing around the flag for injection so that tactics calling inj atHugo Herbelin
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.
2017-10-25Put newlines at the end of files.Gaëtan Gilbert
2017-10-23Move bug files to match their new GitHub ID (fixes #6001).Théo Zimmermann
2017-10-20Merge PR #5989: Handle ∞ in coq-makefile timing test-suiteMaxime Dénès
2017-10-20Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" ↵Maxime Dénès
clause of an inductive definitions
2017-10-19Handle ∞ in coq-makefile timing test-suiteJason Gross
This should (hopefully) fix #5675.
2017-10-19Moving bug numbers to BZ# format in the test-suite.Théo Zimmermann
Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers.
2017-10-17Adding a test for bug BZ#5692.Pierre-Marie Pédrot
2017-10-15[stdlib] Fix warnings on deprecated `Add Setoid`Emilio Jesus Gallego Arias
The test suite cases are preserved until the feature is actually removed.
2017-10-10Use a nice printer for constant names in Suggest Proof Using.Gaëtan Gilbert
2017-10-10Take Suggest Proof Using outside the kernel.Gaëtan Gilbert
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"
2017-10-10Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Maxime Dénès
2017-10-09Merge PR #1126: [ltac] Warning for deprecated `Add Setoid` and `Add ↵Maxime Dénès
Morphism` forms.
2017-10-09Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for ↵Maxime Dénès
printing-ony Notations
2017-10-06Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type ↵Maxime Dénès
"_something")
2017-10-06Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ↵Maxime Dénès
inductive definition)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 15:08:32 +0000