| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-24 | Fix #7323: coqchk puts polymorphic univs of inductive in global env | Gaëtan Gilbert | |
| 2018-05-24 | Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constants | Pierre-Marie Pédrot | |
| 2018-05-24 | Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant ↵ | Pierre-Marie Pédrot | |
| instances | |||
| 2018-05-23 | Merge PR #7567: Clean-up dead file in test-suite. | Enrico Tassi | |
| 2018-05-20 | Add test cases from #7554 | Tej Chajed | |
| Failed in v8.7.2 but were fixed by v8.8.0. | |||
| 2018-05-18 | Clean-up dead file in test-suite. | Théo Zimmermann | |
| 2018-05-17 | Merge PR #7451: Introduce an option to allow nested lemma, and turn it off ↵ | Emilio Jesus Gallego Arias | |
| by default. | |||
| 2018-05-17 | Introduce an option to allow nested lemma, and turn it off by default. | Théo Zimmermann | |
| 2018-05-16 | Modify make system to include Makefile.common in the test suite | Gaëtan Gilbert | |
| 2018-05-16 | unit tests: add .merlin | Gaëtan Gilbert | |
| 2018-05-16 | add unit tests to test suite | Paul Steckler | |
| 2018-05-16 | Merge PR #7484: Fix non-portable shebang in test-suite. | Enrico Tassi | |
| 2018-05-15 | [ssr] import ssreflect test suite from math-comp | Enrico Tassi | |
| 2018-05-14 | Merge PR #7502: Fixing little printing bug with "Locate" on recursive notations | Emilio Jesus Gallego Arias | |
| 2018-05-14 | Merge PR #7479: Move 4722 (dangling symlink) to misc tests, remove dangling ↵ | Gaëtan Gilbert | |
| symlink from repo | |||
| 2018-05-13 | Fixing a bug in printing the body of a located notation. | Hugo Herbelin | |
| This was introduced between v8.5 and v8.6 (presumably 63f3ca8). | |||
| 2018-05-13 | Move 4722 (dangling symlink) to misc tests, remove dangling symlink from repo | Ralf Jung | |
| Fixes #7065 | |||
| 2018-05-13 | Merge PR #7477: Support for notations with autonomous only-parsing and ↵ | Emilio Jesus Gallego Arias | |
| only-printing declarations. | |||
| 2018-05-11 | Merge PR #7470: use at least 6 Xs in mktemp filename templates | Gaëtan Gilbert | |
| 2018-05-11 | Fix non-portable shebang in test-suite. | Théo Zimmermann | |
| 2018-05-11 | Merge PR #7363: [ci] Fix another issue with the timing tests | Gaëtan Gilbert | |
| 2018-05-10 | Fixes #7462, part 2 (only-printing not make believe parsing rule is declared). | Hugo Herbelin | |
| 2018-05-10 | Fixes part 1 of #7462 (only-printing not to override existing interp rule). | Hugo Herbelin | |
| 2018-05-09 | use at least 6 Xs in mktemp filename templates | Sven M. Hallberg | |
| OpenBSD mktemp fails with an error otherwise. | |||
| 2018-05-09 | test for coqc -o | Enrico Tassi | |
| 2018-05-03 | Merge PR #7134: When an error comes from loading the prelude, tell it ↵ | Emilio Jesus Gallego Arias | |
| happened at initialization time | |||
| 2018-05-02 | Making explicit that errors happen in one of five executation phases. | Hugo Herbelin | |
| The five phases are command line interpretation, initialization, prelude loading, rcfile loading, and sentence interpretation (only the two latters are located). We then parameterize the feedback handler with the given execution phase, so as to possibly annotate the message with information pertaining to the phase. | |||
| 2018-05-02 | Make "intro"/"intros" progress on existential variables. | Hugo Herbelin | |
| 2018-04-29 | Strict focusing using Default Goal Selector. | Gaëtan Gilbert | |
| We add a [SelectAlreadyFocused] constructor to [goal_selector] (read "!") which causes a failure when there's not exactly 1 goal and otherwise is a noop. Then [Set Default Goal Selector "!".] puts us in "strict focusing" mode where we can only run tactics if we have only one goal or use a selector. Closes #6689. | |||
| 2018-04-26 | [ci] Fix another issue with the timing tests | Jason Gross | |
| There was recently a spurious failure on AppVeyor (I've forgotten which PR). This commit fixes that particular failure. | |||
| 2018-04-26 | Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars. | Hugo Herbelin | |
| 2018-04-23 | Fix #7327: coqchk subtyping of polymorphic constants | Gaëtan Gilbert | |
| 2018-04-22 | test suite: clean more things (glob, MExtraction.out, distclean aux) | Gaëtan Gilbert | |
| NB: I made .aux be cleaned only with distclean imitating the main Makefile. | |||
| 2018-04-22 | test suite: print message for failing tests as they come | Gaëtan Gilbert | |
| ie you might see make TEST bugs/closed/1337.v TEST bugs/closed/3263.v TEST bugs/closed/7777.v FAILED bugs/closed/3263.v.log TEST bugs/opened/1.v ... report: 3263 failed (should be closed) | |||
| 2018-04-22 | test suite Makefile: do not use %.stamp for subsystem targets | Gaëtan Gilbert | |
| 2018-04-20 | Fix #6798: coqchk ignores ugraph when comparing constant instances | Gaëtan Gilbert | |
| 2018-04-16 | Merge PR #7237: [ssr] fix delayed clears (fix #7045) | Maxime Dénès | |
| 2018-04-13 | [ltac] Deprecate nameless fix/cofix. | Emilio Jesus Gallego Arias | |
| LTAC's `fix` and `cofix` do require access to the proof object inside the tactic monad when used without a name. This is a bit inconvenient as we aim to make the handling of the proof object purely functional. Alternatives have been discussed in #7196, and it seems that deprecating the nameless forms may have the best cost/benefit ratio, so opening this PR for discussion. See also #6171. | |||
| 2018-04-13 | [ssr] fix delayed clears (fix #7045) | Enrico Tassi | |
| We take into account all future ipats, not just the ones in the current branch | |||
| 2018-04-12 | Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by ↵ | Jason Gross | |
| removing the test. | |||
| 2018-04-12 | Merge PR #500: Move bugs that have been closed on Bugzilla | Maxime Dénès | |
| 2018-04-12 | Merge PR #7087: Congruence tactic engine update | Pierre-Marie Pédrot | |
| 2018-04-11 | Fix the status of some resolved bugs | Tej Chajed | |
| 2018-04-09 | Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while ↵ | Emilio Jesus Gallego Arias | |
| looking for a notation for a nested pattern | |||
| 2018-04-09 | Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilation | Pierre-Marie Pédrot | |
| 2018-04-09 | Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050) | Maxime Dénès | |
| 2018-04-06 | Fix #6956: Uncaught exception in bytecode compilation | Maxime Dénès | |
| We also make the code of [compact] in kernel/univ.ml a bit clearer. | |||
| 2018-04-05 | Improve shell scripts | zapashcanon | |
| 2018-04-05 | Fix #5981, bugs/opened/3263.v is non-deterministic by removing the test. | Théo Zimmermann | |
| Since this is an open bug, it is of lesser importance but non-deterministic tests are a real problem OTOH. | |||
| 2018-04-04 | Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context. | Hugo Herbelin | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite