aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...Gravatar Matthieu Sozeau2018-06-25
|\
* \ Merge PR #7559: Existing Class noop when already a class + warning.Gravatar Matthieu Sozeau2018-06-25
|\ \
* \ \ Merge PR #7620: [ssr] rewrite: turn anomaly into regular errorGravatar Maxime Dénès2018-06-25
|\ \ \
* \ \ \ Merge PR #7236: [ssr] simpler semantics for delayed clearsGravatar Maxime Dénès2018-06-23
|\ \ \ \
| | | | * Remove hack skipping comparison of algebraic universes in subtyping.Gravatar Gaëtan Gilbert2018-06-22
| * | | | [ssr] implement {}/v as a short hand for {v}/v when v is an idGravatar Enrico Tassi2018-06-22
| | |_|/ | |/| |
* / | | [ssr] test case for rewrite and set on univ poly keysGravatar Enrico Tassi2018-06-22
|/ / /
| * / [ssr] test case for rewrite (setoid) making the goal illtypedGravatar Enrico Tassi2018-06-20
|/ /
* | 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
|/ / / / /
| | | | * Existing Class noop when already a class + warning.Gravatar Gaëtan Gilbert2018-06-08
| |_|_|/ |/| | |
* | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 20:49:45 +0000