aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Merge PR #6754: Better elaboration of pattern-matchings on primitive projectionsGravatar Pierre-Marie Pédrot2018-06-19
|\
* | Fix #7421: constr_eq ignores universe constraints.Gravatar Gaëtan Gilbert2018-06-18
* | Merge PR #7824: Fixes #7811 (uncaught Not_found in notation printer related t...Gravatar Pierre-Marie Pédrot2018-06-17
|\ \
* \ \ Merge PR #7818: Do not allow spliting in res_pf, this is reserved for pretypingGravatar Pierre-Marie Pédrot2018-06-17
|\ \ \
| | * | Fixes #7811 (uncaught Not_found in notation printer related to "match").Gravatar Hugo Herbelin2018-06-17
| |/ / |/| |
* | | Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.Gravatar Maxime Dénès2018-06-17
|\ \ \
| | | * Add test-suite case for performance, had to use TimeoutGravatar Matthieu Sozeau2018-06-15
| | | * Better elaboration of pattern-matchings on primitive projectionsGravatar Matthieu Sozeau2018-06-15
| |_|/ |/| |
| | * Do not allow spliting in res_pf, this is reserved for pretypingGravatar Matthieu Sozeau2018-06-15
* | | Workaround to handle non-value arguments in tactics.Gravatar Cyprien Mangin2018-06-14
| |/ |/|
* | Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...Gravatar Pierre-Marie Pédrot2018-06-14
|\ \
* \ \ Merge PR #664: Fixing #5500 (missing test in return clause of match leading t...Gravatar Matthieu Sozeau2018-06-14
|\ \ \
* \ \ \ Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder i...Gravatar Matthieu Sozeau2018-06-14
|\ \ \ \
* \ \ \ \ Merge PR #7771: Tweak printing boxes for unicode bindersGravatar Hugo Herbelin2018-06-14
|\ \ \ \ \
* | | | | | Markdown docs: switch from absolute to relative links.Gravatar Théo Zimmermann2018-06-13
* | | | | | Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").Gravatar Hugo Herbelin2018-06-12
| | * | | | Fixes #7780 (missing lift in expanding alias under a binder in unification).Gravatar Hugo Herbelin2018-06-12
| |/ / / / |/| | | |
| * | | | Tweak printing boxes for unicode bindersGravatar Ralf Jung2018-06-10
* | | | | Fixing #7700 (section variables bound to abbreviations were not found).Gravatar Hugo Herbelin2018-06-10
|/ / / /
* | | | add test for #7595Gravatar Ralf Jung2018-06-07
| | | * Fix #7615: Functor inlining drops universe substitution.Gravatar Pierre-Marie Pédrot2018-06-07
| |_|/ |/| |
* | | Merge PR #7077: Preserving canonical structure of return predicate in vm_comp...Gravatar Maxime Dénès2018-06-05
|\ \ \
* \ \ \ Merge PR #7663: test suite: make target to regenerate failing output testsGravatar Enrico Tassi2018-06-05
|\ \ \ \
* | | | | Fix #7631: native_compute fails to compile an example in Coq 8.8Gravatar Maxime Dénès2018-06-04
* | | | | Merge PR #7315: An attempt to clarify error message for Arguments needing "re...Gravatar Maxime Dénès2018-06-04
|\ \ \ \ \
| | | * | | Tests for part of #7068 and for #7076 (vm/native_compute and return predicate).Gravatar Hugo Herbelin2018-06-04
| |_|/ / / |/| | | |
* | | | | Merge PR #7229: Deprecate implicit tactic solving.Gravatar Hugo Herbelin2018-06-04
|\ \ \ \ \
| | | * | | test suite: make target to regenerate failing output testsGravatar Gaëtan Gilbert2018-06-04
* | | | | | Merge PR #7199: Fixes #7195: missing freshness condition in Ltac pattern-matc...Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomalyGravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #7189: Fix #5539: algebraic universe produced by cases.Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ta...Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct...Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".Gravatar Matthieu Sozeau2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | | Deprecate implicit tactic solving.Gravatar Pierre-Marie Pédrot2018-06-04
| |_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | |
* | | | | | | | | | | | Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.Gravatar Maxime Dénès2018-06-04
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | |
* | | | | | | | | | | | Merge PR #7578: Allow make clean to work on a fresh cloneGravatar Enrico Tassi2018-05-31
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | * | | | | | Fix #7113: Program Let Fixpoint in section causes anomalyGravatar Gaëtan Gilbert2018-05-30
* | | | | | | | | | | | | Fix #6951: Unexpected error during scheme creation.Gravatar Pierre-Marie Pédrot2018-05-29
| |_|_|_|_|_|/ / / / / / |/| | | | | | | | | | |
* | | | | | | | | | | | Add test for #7333: vm_compute segfaults / Anomaly with cofixGravatar Maxime Dénès2018-05-29
| * | | | | | | | | | | Allow make clean to work on a fresh cloneGravatar Jason Gross2018-05-25
| | | | | | | | | * | | An attempt to clarify error message for Arguments needing "rename" flag.Gravatar Hugo Herbelin2018-05-25
| |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | |
* | | | | | | | | | | Fix #7323: coqchk puts polymorphic univs of inductive in global envGravatar Gaëtan Gilbert2018-05-24
* | | | | | | | | | | Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constantsGravatar Pierre-Marie Pédrot2018-05-24
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant inst...Gravatar Pierre-Marie Pédrot2018-05-24
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | | * | | | | | | | Fix #7586: Anomaly "Uncaught exception Not_found".Gravatar Pierre-Marie Pédrot2018-05-23
| |_|_|_|/ / / / / / / / |/| | | | | | | | | | |
* | | | | | | | | | | | Merge PR #7567: Clean-up dead file in test-suite.Gravatar Enrico Tassi2018-05-23
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / / / |/| | | | | | | | | | |
* | | | | | | | | | | | Add test cases from #7554Gravatar Tej Chajed2018-05-20
| | | | | * | | | | | | Fix #7539: Checker does not properly handle negative coinductive types.Gravatar Pierre-Marie Pédrot2018-05-18
| |_|_|_|/ / / / / / / |/| | | | | | | | | |