aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
Commit message (Collapse)AuthorAge
* Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Maxime Dénès2018-02-19
|\
* \ Merge PR #6753: [toplevel] Make toplevel state into a record.Gravatar Maxime Dénès2018-02-19
|\ \
* \ \ Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵Gravatar Maxime Dénès2018-02-19
|\ \ \ | | | | | | | | | | | | camlp4
* \ \ \ Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.Gravatar Maxime Dénès2018-02-19
|\ \ \ \
| | * | | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | | | | | | | | | | | | | | | | | longer use camlp4.
| | | * | [toplevel] Make toplevel state into a record.Gravatar Emilio Jesus Gallego Arias2018-02-15
| |_|/ / |/| | | | | | | | | | | | | | | | | | | 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.
| * | | coqdev.el: wait for 'compile to touch compilation-error-regexp-alistGravatar Gaëtan Gilbert2018-02-13
| | | | | | | | | | | | | | | | (and alist-alist)
| * | | coqdev.el: fix "compilate"-command typoGravatar Gaëtan Gilbert2018-02-13
| | | |
| * | | coqdev.el: shell-quote-argument the directory for make -CGravatar Gaëtan Gilbert2018-02-13
| | | |
| * | | coqdev.el: stop using when-let for emacs<25 compatibility.Gravatar Gaëtan Gilbert2018-02-13
| | | |
| | | * [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | Merge PR #6565: [Backport script] Check .mli files are not changed.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ | |_|_|/ |/| | |
* | | | Merge PR #6718: Fix redirection to stderr in lint-repository error message.Gravatar Maxime Dénès2018-02-12
|\ \ \ \
* \ \ \ \ Merge PR #6706: ci-common: guess CI_BRANCH for local buildsGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ | |_|_|_|/ |/| | | |
| | | | * Merge anomaly-traces-parser.el into coqdev.el.Gravatar Gaëtan Gilbert2018-02-11
| | | | |
| | | | * coqdev.el: add installation instructions.Gravatar Gaëtan Gilbert2018-02-11
| | | | |
| | * | | Fix redirection to stderr in lint-repository error message.Gravatar Gaëtan Gilbert2018-02-08
| |/ / / |/| | |
* | | | Merge PR #6610: Points to Flocq official repository.Gravatar Maxime Dénès2018-02-07
|\ \ \ \
* \ \ \ \ Merge PR #6686: Kernel/checker reduction cleanups around projection unfoldingGravatar Maxime Dénès2018-02-07
|\ \ \ \ \
| | | * | | ci-common: guess CI_BRANCH for local buildsGravatar Gaëtan Gilbert2018-02-07
| |_|/ / / |/| | | |
* | | | | Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.Gravatar Maxime Dénès2018-02-06
|\ \ \ \ \
| | | * | | Points to Flocq official repository.Gravatar Théo Zimmermann2018-02-05
| |_|/ / / |/| | | | | | | | | | | | | | Following comment at https://github.com/coq/coq/pull/6596#issuecomment-358246528.
| | * | | Add overlay for equations (nf_beta takes an env)Gravatar Gaëtan Gilbert2018-02-05
| | | | |
* | | | | Merge PR #6654: CI: Run coqchk on IrisGravatar Maxime Dénès2018-02-05
|\ \ \ \ \ | |_|/ / / |/| | | |
| | * | | [stm] [toplevel] Make loadpath a parameter of the document.Gravatar Emilio Jesus Gallego Arias2018-02-05
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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...
| * | | CI: Run coqchk on IrisGravatar Ralf Jung2018-01-31
| | | |
* | | | Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing ↵Gravatar Maxime Dénès2018-01-31
|\ \ \ \ | | | | | | | | | | | | | | | menhir.
* \ \ \ \ 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 #6605: Safer VM interfacesGravatar Maxime Dénès2018-01-30
|\ \ \ \ \
| * | | | | Safer VM interfacesGravatar Maxime Dénès2018-01-26
| | |/ / / | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* / | | | Use travis_retry on apt-get updateGravatar Jason Gross2018-01-23
|/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | Merge PR #6629: Archive COMPATIBILITYGravatar Maxime Dénès2018-01-23
|\ \ \ \
* \ \ \ \ Merge PR #6568: Cleanup scriptsGravatar Maxime Dénès2018-01-23
|\ \ \ \ \
| | * | | | Archive COMPATIBILITY.Gravatar Théo Zimmermann2018-01-22
| | | | | |
* | | | | | Merge PR #6550: Remove outdated note about rlwrap in setup.txtGravatar Maxime Dénès2018-01-22
|\ \ \ \ \ \ | |_|/ / / / |/| | | | |
* | | | | | Merge PR #6448: Cleanup and add debug printers a bitGravatar Maxime Dénès2018-01-18
|\ \ \ \ \ \
| | | * | | | merge-pr.sh: use git diff --quietGravatar Gaëtan Gilbert2018-01-16
| | | | | | |
| | | * | | | Source basic overlay before user overlays.Gravatar Gaëtan Gilbert2018-01-16
| | | | | | |
| | | * | | | Cleanup shell expansions and quoting.Gravatar Gaëtan Gilbert2018-01-16
| | | | | | |
| | | * | | | Simplify logic and streamline lint-repository.shGravatar Gaëtan Gilbert2018-01-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We inline should-check-whitespace.sh in check-eof-newline.sh simplifying the find invocation.
* | | | | | | Fix the wrapper around ocamldebug.Gravatar Pierre-Marie Pédrot2018-01-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since 5ffa147, there is a new clib folder that needed to be added to the set of includes of ocamldebug
* | | | | | | Merge PR #6483: Strong invariants in polymorphic definitionsGravatar Maxime Dénès2018-01-12
|\ \ \ \ \ \ \
| * | | | | | | Adding a custom Travis overlay for HoTT.Gravatar Pierre-Marie Pédrot2018-01-11
| | | | | | | |
* | | | | | | | Merge PR #6557: First stab at documenting the test suite.Gravatar Maxime Dénès2018-01-11
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6519: Python script checking missing/unnecessary [needs: rebase] labelGravatar Maxime Dénès2018-01-10
|\ \ \ \ \ \ \ \ \ | |_|/ / / / / / / |/| | | | | | | |
| | | | | | | * | [Backport script] Check .mli files are not changed.Gravatar Théo Zimmermann2018-01-09
| |_|_|_|_|_|/ / |/| | | | | | |
| | | | | * | | Cleanup conditional in lint-repository.shGravatar Gaëtan Gilbert2018-01-08
| | | | | |/ /
| | | | * / / Stop talking about debian in "A note about rlwrap"Gravatar Gaëtan Gilbert2018-01-08
| | | | |/ / | | | | | | | | | | | | | | | | | | Debian stable version is 0.42-3 right now.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 08:47:21 +0000