aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Merge PR #7964: Document that GITURL variables shouldn't have a trailing ↵Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ | | | | | | .git anymore.
* \ Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, ↵Gravatar Emilio Jesus Gallego Arias2018-07-01
|\ \ | | | | | | | | | Z into three files
| | * Document that GITURL variables shouldn't have a trailing .git anymore.Gravatar Théo Zimmermann2018-06-29
| |/ |/| | | | | This allows to append /archive at the end.
* | Merge PR #7918: Mini-update of version history with recent changes.Gravatar Théo Zimmermann2018-06-29
|\ \
| | * Splitting primitive numeral parser/printer for positive, N, Z into three files.Gravatar Hugo Herbelin2018-06-29
| | |
* | | Merge PR #7080: Swapping Context and Constr and defining declarations on ↵Gravatar Maxime Dénès2018-06-29
|\ \ \ | | | | | | | | | | | | constr in Constr
* \ \ \ Merge PR #7745: Make type Environ.globals abstract + simplify ↵Gravatar Maxime Dénès2018-06-29
|\ \ \ \ | |_|_|/ |/| | | | | | | Environ.retroknowledge
* | | | Merge PR #7928: Fix 'unbound variable' issue on Windows packaging jobs.Gravatar Michael Soegtrop2018-06-28
|\ \ \ \
* \ \ \ \ Merge PR #7917: Critical bugs: added #3243 and Gonthier's bug in lazy machine.Gravatar Théo Zimmermann2018-06-28
|\ \ \ \ \
| | | * | | Make Environ.globals abstract.Gravatar Gaëtan Gilbert2018-06-28
| |_|/ / / |/| | | |
* | | | | Add mit-plv/bedrock2-ci to CIGravatar Andres Erbsen2018-06-27
| | | | |
| | | * | Adding overlay.Gravatar Hugo Herbelin2018-06-27
| | | | |
| | | * | Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
| |_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This shall eventually allow to use contexts of declarations in the definition of the "Case" constructor. Basically, this means that Constr now includes Context and that the "t" types of Context which were specialized on constr are not defined in Constr (unfortunately using a heavy boilerplate).
| | * | Fix 'unbound variable' issue on Windows packaging jobs.Gravatar Théo Zimmermann2018-06-27
| | | |
* | | | Merge PR #7863: Remove Sorts.contentsGravatar Pierre-Marie Pédrot2018-06-27
|\ \ \ \ | |_|/ / |/| | |
* | | | Merge PR #7906: universes_of_constr don't include universes of monomorphic ↵Gravatar Pierre-Marie Pédrot2018-06-26
|\ \ \ \ | | | | | | | | | | | | | | | constants
* \ \ \ \ Merge PR #7831: Fix for issue #7707: include Ltac2 and Equations in Windows ↵Gravatar Maxime Dénès2018-06-26
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | build
* \ \ \ \ \ Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things.Gravatar Maxime Dénès2018-06-26
|\ \ \ \ \ \
| | | | * | | Add overlay for elpiGravatar Gaëtan Gilbert2018-06-26
| | | | | | |
| | | | * | | Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
| |_|_|/ / / |/| | | | |
| | | * | | Add overlay for Equations, ElpiGravatar Gaëtan Gilbert2018-06-26
| | | | | |
| | * | | | Activate the build of Ltac2 and Equations in the Windows installer.Gravatar Théo Zimmermann2018-06-25
| | | | | |
| | * | | | Reuse CI info to know which version of plugins to build on Windows.Gravatar Théo Zimmermann2018-06-25
| | | | | |
| | * | | | Fix for issue 7707: include Ltac2 and Equations in Windows buildGravatar Michael Soegtrop2018-06-25
| |/ / / / |/| | | | | | | | | | | | | | On the way I also fixed some minor issues with calling MakeCoq_MinGW from cygwin.
| | | | * Mini-update of version history with recent changes.Gravatar Hugo Herbelin2018-06-25
| |_|_|/ |/| | |
| | | * Critical bugs: added #3243 and Gonthier's bug in lazy machine.Gravatar Hugo Herbelin2018-06-25
| |_|/ |/| | | | | | | | Both reminded by Enrico.
* | | Merge PR #7895: Revert "Add a note about [ci skip] in CI README."Gravatar Emilio Jesus Gallego Arias2018-06-24
|\ \ \
* \ \ \ Merge PR #7805: Towards listing the critical bugs of the history of Coq.Gravatar Théo Zimmermann2018-06-24
|\ \ \ \
* \ \ \ \ Merge PR #7893: Update dpdgraph branch nameGravatar Théo Zimmermann2018-06-22
|\ \ \ \ \ | |_|_|_|/ |/| | | |
| | | * | Revert "Add a note about [ci skip] in CI README."Gravatar Théo Zimmermann2018-06-22
| |_|/ / |/| | | | | | | | | | | This reverts commit 3a44a190a7f5d057b6a4bcb50124b42d83f3d03d.
| | | * Fix Windows install script following removal of INSTALL.ide and move of ↵Gravatar Théo Zimmermann2018-06-22
| |_|/ |/| | | | | | | | INSTALL.doc.
* | | Merge PR #7774: [build] Fix checks and notes noting 4.02.1 instead of 4.02.3Gravatar Maxime Dénès2018-06-21
|\ \ \
| | * | Update dpdgraph branch nameGravatar Gaëtan Gilbert2018-06-21
| |/ / |/| | | | | | | | See https://github.com/Karmaki/coq-dpdgraph/issues/50 for context
* | | Merge PR #7797: Remove reference name type.Gravatar Enrico Tassi2018-06-19
|\ \ \
| * | | Overlay for reference removalGravatar Maxime Dénès2018-06-18
| | | |
* | | | Update section on adding your project to CI and link to example PR.Gravatar Théo Zimmermann2018-06-18
| | | |
| * | | Remove reference name type.Gravatar Maxime Dénès2018-06-18
|/ / / | | | | | | | | | | | | | | | | | | | | | reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
* | | Merge PR #7752: [merge script] Check if the CI that was run is outdated.Gravatar Maxime Dénès2018-06-17
|\ \ \
| | | * Very first try at listing the critical bugs of the history of Coq.Gravatar Hugo Herbelin2018-06-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | I let open several questions about fixes to the kernel which maybe were not critical. I skipped what seemed to have been bugs in beta-releases. Need double-checks, decision about the format, etc.
* | | | Merge PR #7793: [ci] update docker image to include elpi 1.0.4Gravatar Emilio Jesus Gallego Arias2018-06-14
|\ \ \ \
* \ \ \ \ Merge PR #664: Fixing #5500 (missing test in return clause of match leading ↵Gravatar Matthieu Sozeau2018-06-14
|\ \ \ \ \ | |_|_|_|/ |/| | | | | | | | | to anomaly)
| | * | | [ci] update docker image to include elpi 1.0.4Gravatar Enrico Tassi2018-06-13
| | | | |
* | | | | Document how to restart failed CI jobs.Gravatar Théo Zimmermann2018-06-13
| | | | | | | | | | | | | | | | | | | | [ci skip]
* | | | | Markdown docs: switch from absolute to relative links.Gravatar Théo Zimmermann2018-06-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We had mostly used absolute links in the past. I just discovered that GitHub recommends using relative links instead: https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links and indeed my Emacs Markdown mode can handle relative links but doesn't interpret absolute links relatively to the root of the git repository. [ci skip]
* | | | | [api] Add compatiblity Misctypes module.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | | | | | | | | | | | | | | | | | | | To be removed in 8.10.
* | | | | [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
| |/ / / |/| | | | | | | | | | | | | | | - move_location to proofs/logic. - intro_pattern_naming to Namegen.
* | | | Merge PR #6827: [VM] Remove projection names from structured constants.Gravatar Pierre-Marie Pédrot2018-06-11
|\ \ \ \
| | | | * [build] Fix checks and notes noting 4.02.1 instead of 4.02.3Gravatar Emilio Jesus Gallego Arias2018-06-11
| |_|_|/ |/| | | | | | | | | | | | | | | Bumping to 4.02.3 was decided some time ago in the WG, however a couple of places escaped updating.
* | | | [ci] GeoCoq now depends on math-comp's ssralg.Gravatar Emilio Jesus Gallego Arias2018-06-11
| | | |
| * | | [VM] Remove projection names from structured constants.Gravatar Maxime Dénès2018-06-10
|/ / / | | | | | | | | | | | | | | | | | | It was actually a hack since those names are never used to represent values, only to be passed as arguments to bytecode instructions. So instead of reusing the structured_constant type, we follow the same pattern as switch annotations.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 19:55:20 +0000