aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Tactic deprecation machineryGravatar Maxime Dénès2018-07-12
* Merge PR #7920: Generic syntax for attributesGravatar Maxime Dénès2018-07-09
|\
* \ Merge PR #7884: Fix #5719: Uncaught exception Invalid_argument.Gravatar Matthieu Sozeau2018-07-09
|\ \
* | | Add test for #8004.Gravatar Gaëtan Gilbert2018-07-06
* | | Convert timing tools to run with both python2 and python3Gravatar Jasper Hugunin2018-07-04
| | * [test suite] Test case for attributesGravatar Vincent Laporte2018-07-03
| |/ |/|
* | Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsGravatar Pierre-Marie Pédrot2018-07-03
|\ \
| * | hints: add Hint Variables/Constants Opaque/Transparent commandsGravatar Matthieu Sozeau2018-07-02
* | | Add test for Uniform Inductive ParametersGravatar Jasper Hugunin2018-07-01
|/ /
* | Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation f...Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ \
* | | Workaround to fix #7731 (printing not splitting line at break hint).Gravatar Hugo Herbelin2018-06-29
| * | Fixes #7712 (an anomaly in reporting bad recursive notation format).Gravatar Hugo Herbelin2018-06-29
|/ /
* | Merge PR #7860: Fix #7704: Launching coqide through PATH fails.Gravatar Emilio Jesus Gallego Arias2018-06-28
|\ \
* \ \ Merge PR #7866: Implementation of mutual records in the higher strataGravatar Maxime Dénès2018-06-28
|\ \ \
* \ \ \ Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)Gravatar Pierre-Marie Pédrot2018-06-27
|\ \ \ \
| * | | | Test file for #7723Gravatar Maxime Dénès2018-06-27
* | | | | Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).Gravatar Hugo Herbelin2018-06-26
|/ / / /
* | | | 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
|\ \ \ \ \ \
| | | | * | | Adding various tests for mutual records.Gravatar Pierre-Marie Pédrot2018-06-24
| |_|_|/ / / |/| | | | |
* | | | | | Merge PR #7236: [ssr] simpler semantics for delayed clearsGravatar Maxime Dénès2018-06-23
|\ \ \ \ \ \
| | | | | * | Fix #7704: get_toplevel_path needs normalised argv.(0)Gravatar Gaëtan Gilbert2018-06-22
| | | | * | | 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
|/ / / / /
| | | | * Fix #5719: Uncaught exception Invalid_argument.Gravatar Pierre-Marie Pédrot2018-06-21
| |_|_|/ |/| | |
| * | | [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
| |_|/ |/| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-20 04:00:11 +0000