aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2019-01-09Make it possible to pass flags to coq when running test suiteMaxime Dénès
2019-01-08Fix #9272: `Unset Nested Proofs Allowed` does not capture nested `Instance` ↵Maxime Dénès
proofs. We forbid commands that may open proofs inside proofs.
2019-01-08Merge PR #9292: Fixing some wrong scopes of variables in the interpretation ↵Emilio Jesus Gallego Arias
of the "in" clause of a "match"
2019-01-07Merge PR #9241: Fix #9240: Register for IDProp causes anomaly when non constantEnrico Tassi
2019-01-06Reworking error message for unresolved evar subterm of another evar.Hugo Herbelin
This is a reworking of 7fd28dc9: instead of using words such as "domain of", "codomain of" to refer to a position in the instance of the original evar, we simply display the instance and the name of the unresolved evar in this instance. This is both simpler and more informative. (The positional words remain useful for printing the evar_map in debugging though.) In passing, this fixes #8369 (Not_found in printing message about an unresolved subevar). Incidentally add possible breaking while printing "in environment".
2019-01-04Handle local definitions in implicit arguments of InstanceJasper Hugunin
2018-12-30Fixing an interpretation bug of the "in" clause of "match".Hugo Herbelin
- The head of "in" was wrongly considered binding - Aliases in the "in" pattern were not taken into account
2018-12-30Do not take universes into account in lia reification.Pierre-Marie Pédrot
This is slightly blunt, it might be the case that we get delayed constraints that cannot be solved resulting in a later universe inconsistency, but it looks highly unlikely on arithmetical statements. Alternatively we would have threaded the unification state, but this would have required a much deeper change. Fixes #9268.
2018-12-26Merge PR #8734: Make diffs work for more input stringsHugo Herbelin
2018-12-25Fixing printing bug due to using equality ill-checking hash key of kernel name.Hugo Herbelin
Thanks to Georges Gonthier for noticing it. Expanding a few Pervasives.compare at this occasion.
2018-12-22Merge PR #9248: Fix #7904: update proofview env after ltac constr:()Pierre-Marie Pédrot
2018-12-21Fix #9240: Register for IDProp causes anomaly when non constantGaëtan Gilbert
2018-12-21Do not exclude "opened" bugs from reportMaxime Dénès
2018-12-21Merge PR #9182: Stop printing Monomorphic/Polymorphic in Print.Maxime Dénès
2018-12-20Make diffs work for more input stringsJim Fehrle
Diff code uses the lexer to recognize tokens in the inputs, which can be Pp.t's or strings. To add the highlights in the Pp.t, the diff code matches characters in the input to characters in the tokens. Current code fails for inputs containing quote marks or "(*" because the quote marks and comments don't appear in the tokens. This commit adds a "diff mode" to the lexer to return those characters, making the diff routine more robust.
2018-12-20Merge PR #8488: Warning when using automatic template polymorphismPierre-Marie Pédrot
2018-12-20Merge PR #9200: [ssr] make `>` stand aloneMaxime Dénès
2018-12-19Fix #7904: update proofview env after ltac constr:()Gaëtan Gilbert
(in case of side effects) Also: Fix #4781 Fix #4496
2018-12-19Put #[universes(template)] in outputs testsGaëtan Gilbert
2018-12-19Merge PR #9231: Fixes #9229: Infix not robust wrt choice of variable names ↵Pierre-Marie Pédrot
in right-hand side
2018-12-19coqchk: fix check for kelim with functorsGaëtan Gilbert
2018-12-18Merge PR #9223: Fix universe restriction in delayed mode.Pierre-Marie Pédrot
2018-12-18[ssr] make > a stand alone intro patternEnrico Tassi
2018-12-18Fixes #9229 (Infix not robust wrt choice of variable names).Hugo Herbelin
2018-12-18[ssr] new test by Arthur CharguéraudEnrico Tassi
2018-12-18[ssr] extended intro patterns: + > [^] /ltac:Enrico Tassi
This commit implements the following intro patterns: Temporary "=> +" "move=> + stuff" ==== "move=> tmp stuff; move: tmp" It preserves the original name. "=>" can be chained to force generalization as in "move=> + y + => x z" Tactics as views "=> /ltac:(tactic)" Supports notations, eg "Notation foo := ltac:(bla bla bla). .. => /foo". Limited to views on the right of "=>", views that decorate a tactic as move or case are not supported to be tactics. Dependent "=> >H" move=> >H ===== move=> ???? H, with enough ? to name H the first non-dependent assumption (LHS of the first arrow). TC isntances are skipped. Block intro "=> [^ H] [^~ H]" after "case" or "elim" or "elim/v" it introduces in one go all new assumptions coming from the eliminations. The names are picked from the inductive type declaration or the elimination principle "v" in "elim/v" and are appended/prepended the seed "H" The implementation makes crucial use of the goal_with_state feature of the tactic monad. For example + schedules a generalization to be performed at the end of the intro pattern and [^ .. ] reads the name seeds from the state (that is filled in by case and elim).
2018-12-18Merge PR #9222: Fix classification of Set Default Proof Mode.Enrico Tassi
2018-12-18Merge PR #9160: Avoid user-given names in automatic introduction of bindersPierre-Marie Pédrot
2018-12-17Merge PR #8856: [gitlab] Test Ocaml trunk.Gaëtan Gilbert
2018-12-17Restrict body universes in delayed mode.Gaëtan Gilbert
2018-12-17Stop printing Monomorphic/Polymorphic in Print.Gaëtan Gilbert
You can tell which it is from the `@{}` if you really care, and seeing `Monomorphic List (A:Type)` with no indication that `Monomorphic` is about universes can confuse people.
2018-12-17Fix classification of Set Default Proof Mode.Gaëtan Gilbert
2018-12-17Merge PR #9206: [stm] join the tip of the document even when fixing a proof ↵Emilio Jesus Gallego Arias
(fix #9204)
2018-12-15Avoid explicit names in binders for automatic introsJasper Hugunin
2018-12-14[dune] [gitlab] Test OCaml trunk.Emilio Jesus Gallego Arias
We add a job testing the build of Coq with OCaml 4.08 [AKA `trunk`] CoqIDE is not supported in 4.08 due to missing `lablgtk`, also `oUnit` cannot be currently installed, thus we have to add a switch to the test suite to disable `unit-tests`. Many deprecation warnings happened in 4.08 so we use the `release` profile to make them not fatal. Using a 4.08 build profile would be an option too.
2018-12-13Merge PR #9193: Tests for #4509, #6202 which happen to be fixed (was a lost ↵Gaëtan Gilbert
of evars in shelf)
2018-12-13Merge PR #9117: Accept argument names for extra arguments with "extra scopes"Matthieu Sozeau
2018-12-13Merge PR #9032: checker: check inductive types by roundtrip through the kernel.Pierre-Marie Pédrot
2018-12-13Merge PR #9167: Fixes #9166: no deprecation warning on aliases used as ↵Pierre-Marie Pédrot
pattern variables
2018-12-13[test] for join when error resiliency on and async-proofs offEnrico Tassi
2018-12-13[test] for #9204Enrico Tassi
2018-12-12Accept argument names for extra arguments with "extra scopes"Maxime Dénès
The checks were unnecessarily restrictive (since names can be used for documentation purposes), and the error message was a bit wrong (it mentioned a restriction on the explicit status of arguments).
2018-12-12checker: check inductive types by roundtrip through the kernel.Gaëtan Gilbert
2018-12-12Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`Hugo Herbelin
2018-12-12Fixes #9166 (no warning on pattern variables named like a deprecated alias).Hugo Herbelin
2018-12-12Merge PR #8974: Fix mod_subst wrt universe polymorphismMaxime Dénès
2018-12-11Tests for #4509, #6202 which happen to be fixed (was a lost of evars in shelf).Hugo Herbelin
2018-12-10[test-suite] Fail when the checker failsVincent Laporte
2018-12-10[test-suite] Run `coqchk` on most test casesVincent Laporte
2018-12-08Do so that an error message follows the "Error:" header on the same line.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-13 06:23:43 +0000