| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-06-14 | Workaround to handle non-value arguments in tactics. | Cyprien Mangin | |
| Although the fix is not a proper one, it seems to solve every instance of #2800 that could be tested. | |||
| 2018-06-14 | Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ↵ | Pierre-Marie Pédrot | |
| of submodules. | |||
| 2018-06-14 | Merge PR #664: Fixing #5500 (missing test in return clause of match leading ↵ | Matthieu Sozeau | |
| to anomaly) | |||
| 2018-06-14 | Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder ↵ | Matthieu Sozeau | |
| in unification | |||
| 2018-06-14 | Merge PR #7771: Tweak printing boxes for unicode binders | Hugo Herbelin | |
| 2018-06-13 | Markdown docs: switch from absolute to relative links. | Théo Zimmermann | |
| We had mostly used absolute links in the past. I just discovered that GitHub recommends using relative links instead: https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links and indeed my Emacs Markdown mode can handle relative links but doesn't interpret absolute links relatively to the root of the git repository. [ci skip] | |||
| 2018-06-12 | Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn"). | Hugo Herbelin | |
| This is a quick fix. Code should be made nicer along these lines: - try to pass the name of the variable created by "mkletin_goal" in the monad using "refine_one"; - use a disjunctive type of "inhyps" to indicate when it is meaningful, rather than using []. | |||
| 2018-06-12 | Fixes #7780 (missing lift in expanding alias under a binder in unification). | Hugo Herbelin | |
| 2018-06-10 | Tweak printing boxes for unicode binders | Ralf Jung | |
| 2018-06-10 | Fixing #7700 (section variables bound to abbreviations were not found). | Hugo Herbelin | |
| Redundancy between finding section variables in both interp_var and interp_qualid could probably be cleaned. | |||
| 2018-06-08 | Existing Class noop when already a class + warning. | Gaëtan Gilbert | |
| Fix #5012. | |||
| 2018-06-07 | add test for #7595 | Ralf Jung | |
| 2018-06-07 | Fix #7615: Functor inlining drops universe substitution. | Pierre-Marie Pédrot | |
| We store the universe context in the inlined terms and apply it to the instance provided to the substitution function. Technically the context is not needed, but we use it to assert that the length of the instance corresponds, just in case. | |||
| 2018-06-05 | Merge PR #7077: Preserving canonical structure of return predicate in ↵ | Maxime Dénès | |
| vm_compute and native_compute (partial fix to #7068; also fixes #7076)) | |||
| 2018-06-05 | Merge PR #7663: test suite: make target to regenerate failing output tests | Enrico Tassi | |
| 2018-06-04 | Fix #7631: native_compute fails to compile an example in Coq 8.8 | Maxime Dénès | |
| Dependency analysis for separate compilation was not iterated properly on rel_context and named_context. | |||
| 2018-06-04 | Merge PR #7315: An attempt to clarify error message for Arguments needing ↵ | Maxime Dénès | |
| "rename" flag | |||
| 2018-06-04 | Tests for part of #7068 and for #7076 (vm/native_compute and return predicate). | Hugo Herbelin | |
| 2018-06-04 | Merge PR #7229: Deprecate implicit tactic solving. | Hugo Herbelin | |
| 2018-06-04 | test suite: make target to regenerate failing output tests | Gaëtan Gilbert | |
| 2018-06-04 | Merge PR #7199: Fixes #7195: missing freshness condition in Ltac ↵ | Matthieu Sozeau | |
| pattern-matching names | |||
| 2018-06-04 | Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode. | Matthieu Sozeau | |
| 2018-06-04 | Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomaly | Matthieu Sozeau | |
| 2018-06-04 | Merge PR #7189: Fix #5539: algebraic universe produced by cases. | Matthieu Sozeau | |
| 2018-06-04 | Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ↵ | Matthieu Sozeau | |
| tactic unification. | |||
| 2018-06-04 | Merge PR #7552: Fix #7539: Checker does not properly handle negative ↵ | Matthieu Sozeau | |
| coinductive types. | |||
| 2018-06-04 | Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found". | Matthieu Sozeau | |
| 2018-06-04 | Deprecate implicit tactic solving. | Pierre-Marie Pédrot | |
| 2018-06-04 | Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel. | Maxime Dénès | |
| 2018-05-31 | Merge PR #7578: Allow make clean to work on a fresh clone | Enrico Tassi | |
| 2018-05-30 | Fix #7113: Program Let Fixpoint in section causes anomaly | Gaëtan Gilbert | |
| 2018-05-29 | Fix #6951: Unexpected error during scheme creation. | Pierre-Marie Pédrot | |
| When creating a scheme for bifinite inductive types, we do not create a fixpoint. | |||
| 2018-05-29 | Add test for #7333: vm_compute segfaults / Anomaly with cofix | Maxime Dénès | |
| 2018-05-25 | Allow make clean to work on a fresh clone | Jason Gross | |
| The file `config/Makefile` doesn't exist unless we run `./configure`. We shouldn't have to run `./configure` to run `make clean`. We now no longer error in any case if `config/Makefile` doesn't exist; this is simpler than only not erroring if the target is `clean`. We also now test this property when building on CI. This fixes #7542 | |||
| 2018-05-25 | An attempt to clarify error message for Arguments needing "rename" flag. | Hugo Herbelin | |
| Using a formulation which makes it is clear that no renaming has been done. See discussion at issue #2987. | |||
| 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 | Fix #7586: Anomaly "Uncaught exception Not_found". | Pierre-Marie Pédrot | |
| The old unification engine was using the unfiltered environment when a context had been cleared, leading to an ill-typed goal. | |||
| 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 | Fix #7539: Checker does not properly handle negative coinductive types. | Pierre-Marie Pédrot | |
| The reduction machine of the checker was not taking into account the fact that cofixpoints needed to be unfolded when applied against a projection. | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite