aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* [vernac] Mutual theorems (VernacStartTheoremProof) always have namesGravatar Vincent Laporte2018-02-01
* [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionGravatar Vincent Laporte2018-02-01
* Merge PR #6601: Circle CI: fix cache selection.Gravatar Maxime Dénès2018-01-31
|\
* \ Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing m...Gravatar Maxime Dénès2018-01-31
|\ \
* \ \ Merge PR #6663: [toplevel] Refactor load path handling.Gravatar Maxime Dénès2018-01-31
|\ \ \
* \ \ \ Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees"Gravatar Maxime Dénès2018-01-31
|\ \ \ \
* \ \ \ \ Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Gravatar Maxime Dénès2018-01-31
|\ \ \ \ \
| | | | * | Put default value for NJOBS in ci-common.Gravatar Gaëtan Gilbert2018-01-30
| * | | | | Adding an overlay for Equations.Gravatar Pierre-Marie Pédrot2018-01-30
* | | | | | Merge PR #6666: Fix reduction of primitive projections on coinductive records...Gravatar Maxime Dénès2018-01-30
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6649: Fix #6621: Anomaly on fixpoint with primitive projectionsGravatar Maxime Dénès2018-01-30
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6636: Stop running duplicate Travis jobs on pull requests.Gravatar Maxime Dénès2018-01-30
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6605: Safer VM interfacesGravatar Maxime Dénès2018-01-30
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6644: Use travis_retry on apt-get updateGravatar Maxime Dénès2018-01-30
|\ \ \ \ \ \ \ \ \ \
| | | | | * | | | | | Add test case for #5286.Gravatar Maxime Dénès2018-01-29
| | | | | * | | | | | [cbv] Fix evaluation of cofixpoints under primitive projections.Gravatar Maxime Dénès2018-01-29
| | | | | * | | | | | [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
| |_|_|_|_|_|/ / / |/| | | | | | | |
| | * | | | | | | Safer VM interfacesGravatar Maxime Dénès2018-01-26
| | | | | | * | | 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
| |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 05:00:17 +0000