aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
| | | | | * | | | | | | | | [native_compute] Fix evaluation of cofixpoints under primitive projections.Gravatar Maxime Dénès2018-01-29
| |_|_|_|/ / / / / / / / / |/| | | | | | | | | | | |
| | | | | | | * | | | | | [toplevel] Refactor load path handling.Gravatar Emilio Jesus Gallego Arias2018-01-29
| |_|_|_|_|_|/ / / / / / |/| | | | | | | | | | |
| | | | | | | | | | * | allow vernacular controls before focus selector, issue #6587Gravatar Paul Steckler2018-01-26
| |_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | |
| | * | | | | | | | | Safer VM interfacesGravatar Maxime Dénès2018-01-26
| | | | | | | | | | * document the Fail commandGravatar Paul Steckler2018-01-25
| |_|_|_|_|_|_|_|_|/ |/| | | | | | | | |
| | | | | | * | | | Add test case for #5747Gravatar Maxime Dénès2018-01-25
| | | | | | * | | | [checker] Avoid relying on canonical names.Gravatar Maxime Dénès2018-01-25
| | | | | | * | | | [checker] Remove duplicated functionGravatar Maxime Dénès2018-01-25
| | | | | | * | | | [checker] Better error message for bad recursive treesGravatar Maxime Dénès2018-01-25
| |_|_|_|_|/ / / / |/| | | | | | | |
| * | | | | | | | Add a comment referencing travis issue numbersGravatar Jason Gross2018-01-25
* | | | | | | | | Merge PR #6642: fix space in coqchk errorGravatar Maxime Dénès2018-01-25
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6650: Remove dead code from funind.Gravatar Maxime Dénès2018-01-25
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6626: [readme] Add DOI badge.Gravatar Maxime Dénès2018-01-25
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / / |/| | | | | | | | | |
* | | | | | | | | | | Merge PR #6620: Fix #6591: anomaly when using selectors outside of a proof.Gravatar Maxime Dénès2018-01-25
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | |
| | | | * | | | | | | fix space in coqchk errorGravatar Ralf Jung2018-01-24
| |_|_|/ / / / / / / |/| | | | | | | | |
| | | * | | | | | | Remove dead code from funind.Gravatar Maxime Dénès2018-01-24
| |_|/ / / / / / / |/| | | | | | | |
| | | | | * | | | Fix #6621: Anomaly on fixpoint with primitive projectionsGravatar Maxime Dénès2018-01-24
| |_|_|_|/ / / / |/| | | | | | |
| | | * | | | | Delay installing packagesGravatar Jason Gross2018-01-23
| | | * | | | | Use travis_retry on apt-get updateGravatar Jason Gross2018-01-23
| |_|/ / / / / |/| | | | | |
| | | * | | | Stop running duplicate Travis jobs on pull requests.Gravatar Théo Zimmermann2018-01-23
| |_|/ / / / |/| | | | |
* | | | | | Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for...Gravatar Maxime Dénès2018-01-23
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6628: [printing] Remove duplicate definitions of pr_lident and pr_l...Gravatar Maxime Dénès2018-01-23
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6629: Archive COMPATIBILITYGravatar Maxime Dénès2018-01-23
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6568: Cleanup scriptsGravatar Maxime Dénès2018-01-23
|\ \ \ \ \ \ \ \ \
| | | | | * | | | | Fix #6591: anomaly when using selectors outside of a proof.Gravatar Cyprien Mangin2018-01-22
| | | | | | |_|_|/ | | | | | |/| | |
| | | | | | * | | [readme] Add DOI badge.Gravatar Emilio Jesus Gallego Arias2018-01-22
| | | | | |/ / /
| | * | | | | | Archive COMPATIBILITY.Gravatar Théo Zimmermann2018-01-22
| | * | | | | | Move the mention of the removal of Qed exporting at the right place.Gravatar Théo Zimmermann2018-01-22
| | | |_|/ / / | | |/| | | |
* | | | | | | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Gravatar Maxime Dénès2018-01-22
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6625: Update location on tab switch, issue 6624Gravatar Maxime Dénès2018-01-22
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6576: generate both binary and text annotationsGravatar Maxime Dénès2018-01-22
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6550: Remove outdated note about rlwrap in setup.txtGravatar Maxime Dénès2018-01-22
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.Gravatar Maxime Dénès2018-01-22
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6575: Add flash infos for find and replaceGravatar Maxime Dénès2018-01-22
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6506: Fast rel lookupGravatar Maxime Dénès2018-01-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | |
| | | | | | | | | * | | | [printing] Remove duplicate definitions of pr_lident and pr_lnameGravatar Vincent Laporte2018-01-22
| |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | |
| | | | | | | | | * | | Adding a test for coqchk bug #6619.Gravatar Pierre-Marie Pédrot2018-01-20
| | | | | | | | | * | | Fix #6618: coqchk fails with "ill-typed term".Gravatar Pierre-Marie Pédrot2018-01-20
| | | | | | | | | * | | Remove dead code in Environ.Gravatar Pierre-Marie Pédrot2018-01-20
| |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | |
| | | | | * | | | | | -annotate deprecated. New options: -annot, -bin-annotGravatar Vadim Zaliva2018-01-19
| | | | | | * | | | | update location on tab switch, issue 6624Gravatar Paul Steckler2018-01-19
| |_|_|_|_|/ / / / / |/| | | | | | | | |
| | | * | | | | | | Add test-suite file for issue #6617.Gravatar Cyprien Mangin2018-01-19
| | | * | | | | | | Fix context handling of fix and cofix in Ltac subterm matching.Gravatar Cyprien Mangin2018-01-19
| | | * | | | | | | Define EConstr version of [push_rec_types].Gravatar Cyprien Mangin2018-01-19
| | * | | | | | | | add flash infos about wrap, not found, no. of replacements, no. of finds, iss...Gravatar Paul Steckler2018-01-18
| |/ / / / / / / / |/| | | | | | | |
* | | | | | | | | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Maxime Dénès2018-01-18
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6448: Cleanup and add debug printers a bitGravatar Maxime Dénès2018-01-18
|\ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR #6600: Update configure.ml to only warn on lablgtk >= 2.16.0 and < 2...Gravatar Maxime Dénès2018-01-17
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6593: Add plugins to META.coqGravatar Maxime Dénès2018-01-17
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Gravatar Maxime Dénès2018-01-17
|\ \ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-30 15:56:47 +0000