aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Merge PR #7941: Extend QuestionMark to produce a better error message in ↵Gravatar Pierre-Marie Pédrot2018-07-19
|\ | | | | | | case of missing record field
* \ Merge PR #8054: [dev] Autogenerate OCaml dev files.Gravatar Enrico Tassi2018-07-18
|\ \
* | | Remove fourier pluginGravatar Maxime Dénès2018-07-17
| | | | | | | | | | | | As stated in the manual, the fourier tactic is subsumed by lra.
| | * Add overlay for Coq-Equations for QuestionMark.Gravatar Siddharth Bhat2018-07-17
| |/ |/| | | | | | | The changed QuestionMark structure breaks Coq-Equations. Add an overlay to fix this.
* | Only check overlay extensions on git-tracked filesGravatar Jason Gross2018-07-16
| | | | | | | | | | This way, when editors leave over temporary files from editing user-overlays, we don't prevent commits unless they are added to git.
| * [dev] Autogenerate OCaml dev files.Gravatar Emilio Jesus Gallego Arias2018-07-12
|/ | | | | | | | For now we only copy the templates, but we could do more fancy stuff. This helps to be compatible with build systems that take care of these files automatically, see: https://github.com/coq/coq/pull/6857#discussion_r202096579
* Merge PR #8051: Clean-up user-overlays folder.Gravatar Emilio Jesus Gallego Arias2018-07-12
|\
| * Clean-up user-overlays folder.Gravatar Théo Zimmermann2018-07-12
| |
* | [ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0Gravatar Emilio Jesus Gallego Arias2018-07-11
|/ | | | | | - We update the OCaml version used in the base CI image. - Windows / OSX image building is also updated to use newer OCaml. - We also update Dune to 1.0.0.
* Merge PR #7898: Remove camlp4 remainsGravatar Emilio Jesus Gallego Arias2018-07-11
|\
* | Add new options --no-conflict and --no-signature-check to backport script.Gravatar Théo Zimmermann2018-07-10
| |
* | Modify URLs in xml-protocol.mdGravatar Rin Arakaki2018-07-08
| |
* | Modify URLs in xml-protocol.mdGravatar Rin Arakaki2018-07-08
| |
| * Add an overlay.Gravatar Pierre-Marie Pédrot2018-07-07
| |
| * Introduce a Pcoq.Entry module for functions that ought to be exported.Gravatar Pierre-Marie Pédrot2018-07-07
|/ | | | | | | | | | We deprecate the corresponding functions in Pcoq.Gram. The motivation is that the Gram module is used as an argument to Camlp5 functors, so that it is not stable by extension. Enforcing that its type is literally the one Camlp5 expects ensures robustness to extension statically. Some really internal functions have been bluntly removed. It is unlikely that they are used by external plugins.
* Merge PR #7746: Many small cleanups removing unused arguments and functionsGravatar Pierre-Marie Pédrot2018-07-05
|\
* \ Merge PR #7979: TACTIC EXTEND in coqppGravatar Emilio Jesus Gallego Arias2018-07-05
|\ \
* | | [ci] Avoid annoying detached head warning.Gravatar Emilio Jesus Gallego Arias2018-07-04
| | |
* | | Merge PR #7978: [ci] [docker] Make sure we don't install optional packages ↵Gravatar Gaëtan Gilbert2018-07-03
|\ \ \ | | | | | | | | | | | | with apt.
| | | * Add overlay for equations.Gravatar Gaëtan Gilbert2018-07-03
| |_|/ |/| |
* | | Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsGravatar Pierre-Marie Pédrot2018-07-03
|\ \ \
| | * | [ci] [docker] Make sure we don't install optional packages with apt.Gravatar Emilio Jesus Gallego Arias2018-07-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This should help towards ensuring that the system only has the packages we specify in the Dockerfile. We were missing: - `git`: used in the CI system itself! - `rsync`: used in the test-suite - `python3-setuptools`, `python3-wheel`: necessary to use pip3 properly to install the missing python package. - `autoconf`, `automake`: a few CI contribs depend on them.
| | | * Documenting the syntax changes.Gravatar Pierre-Marie Pédrot2018-07-02
| | |/
| * / Add Equations overlayGravatar Matthieu Sozeau2018-07-02
| |/
* / Clean up documentation around beginner's guide.Gravatar Siddharth Bhat2018-07-02
|/ | | | | | | | | - move `README` to `README.md` to take advantage of markdown features - remove `setup.txt`, port the editor specific information to the wiki. Merge development information into `dev/doc/README.md`. Wiki merge link: https://github.com/coq/coq/wiki/DevelSetup. - Add new links to files into `dev/README.md`. - Remove stale `translate.txt`.
* Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵Gravatar Emilio Jesus Gallego Arias2018-07-02
|\ | | | | | | points of Camlp5
* \ 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
| | | * Adding an overlay for the PR.Gravatar Pierre-Marie Pédrot2018-06-29
| | | |
| | | * Documenting the transition strategy of GEXTEND.Gravatar Pierre-Marie Pédrot2018-06-29
| |_|/ |/| |
| | * 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
| | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-27 12:34:06 +0000