| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-02-21 | Merge PR #6767: [ci] add elpi | Maxime Dénès | |
| 2018-02-21 | Merge PR #6283: A pre-commit hook to magically fix whitespace issues. | Maxime Dénès | |
| 2018-02-21 | More accurate and complete headers. | Théo Zimmermann | |
| Remove the mention of specific labs (irrelevant for a copyright notice). Add a mention to represent other contributors and a pointer to CREDITS. | |||
| 2018-02-21 | coqdev.el: add space at the end of compile-command | Gaëtan Gilbert | |
| That way you can just type [-j] instead of having to remember to add a space yourself. | |||
| 2018-02-20 | overlay for ltac2 and Equations | Enrico Tassi | |
| 2018-02-19 | ci: add elpi | Enrico Tassi | |
| 2018-02-19 | Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t` | Maxime Dénès | |
| 2018-02-19 | Merge PR #6753: [toplevel] Make toplevel state into a record. | Maxime Dénès | |
| 2018-02-19 | Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵ | Maxime Dénès | |
| camlp4 | |||
| 2018-02-19 | Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead. | Maxime Dénès | |
| 2018-02-17 | Change references to CAMLP4 to CAMLP5 to be more accurate since we no | Jim Fehrle | |
| longer use camlp4. | |||
| 2018-02-15 | [toplevel] Make toplevel state into a record. | Emilio Jesus Gallego Arias | |
| We organize the toplevel execution as a record and pass it around. This will be used by future PRs as to for example decouple goal printing from the classifier. | |||
| 2018-02-13 | coqdev.el: wait for 'compile to touch compilation-error-regexp-alist | Gaëtan Gilbert | |
| (and alist-alist) | |||
| 2018-02-13 | coqdev.el: fix "compilate"-command typo | Gaëtan Gilbert | |
| 2018-02-13 | coqdev.el: shell-quote-argument the directory for make -C | Gaëtan Gilbert | |
| 2018-02-13 | coqdev.el: stop using when-let for emacs<25 compatibility. | Gaëtan Gilbert | |
| 2018-02-12 | [engine] Remove ghost parameter from `Proofview.Goal.t` | Emilio Jesus Gallego Arias | |
| In current code, `Proofview.Goal.t` uses a phantom type to indicate whether the goal was properly substituted wrt current `evar_map` or not. After the introduction of `EConstr`, this distinction should have become unnecessary, thus we remove the phantom parameter from `'a Proofview.Goal.t`. This may introduce some minor incompatibilities at the typing level. Code-wise, things should remain the same. We thus deprecate `assume`. In a next commit, we will remove normalization as much as possible from the code. | |||
| 2018-02-12 | Merge PR #6565: [Backport script] Check .mli files are not changed. | Maxime Dénès | |
| 2018-02-12 | Tentative fix for #6520: camlcity.org unresponsive makes AppVeyor fail. | Théo Zimmermann | |
| 2018-02-12 | Merge PR #6718: Fix redirection to stderr in lint-repository error message. | Maxime Dénès | |
| 2018-02-12 | Merge PR #6706: ci-common: guess CI_BRANCH for local builds | Maxime Dénès | |
| 2018-02-11 | Merge anomaly-traces-parser.el into coqdev.el. | Gaëtan Gilbert | |
| 2018-02-11 | coqdev.el: add installation instructions. | Gaëtan Gilbert | |
| 2018-02-08 | Fix redirection to stderr in lint-repository error message. | Gaëtan Gilbert | |
| 2018-02-08 | pre-commit: nicer messages | Gaëtan Gilbert | |
| 2018-02-08 | pre-commit: fail gracefully if fixing whitespace removes all changes | Gaëtan Gilbert | |
| 2018-02-08 | pre-commit: add files after fixing ending newlines. | Gaëtan Gilbert | |
| 2018-02-08 | Have the pre-commit hook also fix end-of-file nl | Jason Gross | |
| 2018-02-08 | Auto-create .git/hooks/pre-commit on ./configure | Jason Gross | |
| The hook created checks to see if dev/tools/pre-commit exists, and, if so, runs it. This way, we don't have to do any fancy logic to update the git pre-commit hook. The configure script never overwrites an existing precommit hook, so users can disable it by creating an empty pre-commit hook. The check for existence is so that if users check out an old version of Coq, attempting to commit won't give an error about non-existent files. | |||
| 2018-02-08 | pre-commit hook: fix whitespace error detection | Gaëtan Gilbert | |
| --quiet implies --exit-code | |||
| 2018-02-08 | A pre-commit hook to magically fix whitespace issues. | Gaëtan Gilbert | |
| 2018-02-07 | Merge PR #6610: Points to Flocq official repository. | Maxime Dénès | |
| 2018-02-07 | Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding | Maxime Dénès | |
| 2018-02-07 | ci-common: guess CI_BRANCH for local builds | Gaëtan Gilbert | |
| 2018-02-06 | Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document. | Maxime Dénès | |
| 2018-02-05 | Points to Flocq official repository. | Théo Zimmermann | |
| Following comment at https://github.com/coq/coq/pull/6596#issuecomment-358246528. | |||
| 2018-02-05 | Add overlay for equations (nf_beta takes an env) | Gaëtan Gilbert | |
| 2018-02-05 | Merge PR #6654: CI: Run coqchk on Iris | Maxime Dénès | |
| 2018-02-05 | [stm] [toplevel] Make loadpath a parameter of the document. | Emilio Jesus Gallego Arias | |
| We allow to provide a Coq load path at document creation time. This is natural as the document naming process is sensible to a particular load path, thus clarifying this API point. The changes are minimal, as #6663 did most of the work here. The only point of interest is that we have split the initial load path into two components: - a ML-only load path that is used to locate "plugable" toplevels. - the normal loadpath that includes `theories` and `user-contrib`, command line options, etc... | |||
| 2018-01-31 | CI: Run coqchk on Iris | Ralf Jung | |
| 2018-01-31 | Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing ↵ | Maxime Dénès | |
| menhir. | |||
| 2018-01-31 | Merge PR #6535: Cleanup name-binding structure for fresh evar name generation. | Maxime Dénès | |
| 2018-01-30 | Put default value for NJOBS in ci-common. | Gaëtan Gilbert | |
| 2018-01-30 | Adding an overlay for Equations. | Pierre-Marie Pédrot | |
| 2018-01-30 | Merge PR #6605: Safer VM interfaces | Maxime Dénès | |
| 2018-01-26 | Safer VM interfaces | Maxime Dénès | |
| We separate functions dealing with VM values (vmvalues.ml) and interfaces of the bytecode interpreter (vm.ml). Only the former relies on untyped constructions. This also makes the VM architecture closer to the one of native_compute, another patch could probably try to share more code between the two for conversion and reification (not trivial, though). This is also preliminary work for integers and arrays. | |||
| 2018-01-23 | Use travis_retry on apt-get update | Jason Gross | |
| Script modified from https://unix.stackexchange.com/questions/175146/apt-get-update-exit-status I stuck the code in "install" rather than "before_install" so that the lint target didn't need to be changed. I also haven't touched the targets that add more packages; I'll leave that to someone who knows more about the "&" and "*" syntax being used in the configuration. | |||
| 2018-01-23 | Merge PR #6629: Archive COMPATIBILITY | Maxime Dénès | |
| 2018-01-23 | Merge PR #6568: Cleanup scripts | Maxime Dénès | |
| 2018-01-22 | Archive COMPATIBILITY. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |