aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-09[dune] Build `cmxs` files instead of `cmxa` in "quick" target.Emilio Jesus Gallego Arias
This fixes #8954
2018-11-09Merge PR #8601: Move bound universe names to abstract contextsGaëtan Gilbert
2018-11-09Merge PR #8820: Standardize handling of Automatic Introduction.Pierre-Marie Pédrot
2018-11-09Merge PR #8408: [doc] [ssr] Fix renderingThéo Zimmermann
2018-11-09Add a test for bug #8939.Pierre-Marie Pédrot
2018-11-09Adding an overlay for #8601.Pierre-Marie Pédrot
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
There is little point in having a list, as there is virtually no sharing nor expansion of bound universe names. This representation is thus more compact.
2018-11-09Remove remnants of polymorphic instance name registration.Pierre-Marie Pédrot
2018-11-09Actually store the bound name information in the abstract universe context.Pierre-Marie Pédrot
2018-11-09Force the user to provide names when generating abstract universe contexts.Pierre-Marie Pédrot
For now this data is not stored, but the code checks that indeed the number of names provided coincide with the instance length. I had to reimplement the same kind of workaround hack in section handling as the one already performed in UnivNames because the name information is not present in the section data structure. This deserves a FIXME.
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-11-08Standardize handling of Automatic Introduction.Jasper Hugunin
This fixes #8791. We explicitly specify for intro the names of binders which are given by the user. This still can suffer from spurious collisions, see #8819.
2018-11-09Merge PR #8947: Ensure termination of `file_exists_respecting_case`Emilio Jesus Gallego Arias
2018-11-08Merge PR #8944: Revert PR #8923 (require camlp5 >=7.06)Gaëtan Gilbert
2018-11-08Ensure termination of `file_exists_respecting_case`Vincent Laporte
2018-11-08Merge PR #8098: Update/improve two aspects of the merging process.Maxime Dénès
2018-11-08Revert "Merge PR #8923: Bump camlp5 minimal version and use its safe API."Pierre-Marie Pédrot
This reverts commit c4880effb91fab55c250a799cbceac9b04681db0, reversing changes made to 65927c22bcad62e1bc9a28a57377d82eba215a2d.
2018-11-07Merge PR #8923: Bump camlp5 minimal version and use its safe API.Emilio Jesus Gallego Arias
2018-11-07Merge PR #8934: Revert "Do not allow spliting in res_pf, this is reserved ↵Matthieu Sozeau
for pretyping"
2018-11-07Merge PR #8928: Fixes #8910: typo in nameops.mlPierre-Marie Pédrot
2018-11-07Merge PR #8901: [dune] Add "quick" and "check" targets for fast builds.Gaëtan Gilbert
2018-11-07Merge PR #8927: Optimise git cloningGaëtan Gilbert
2018-11-07Port to safe camlp5 API.Pierre-Marie Pédrot
2018-11-07Bump up the minimal camlp5 version to 7.06.Pierre-Marie Pédrot
This is the first release that contains the type-safe grammar API.
2018-11-07Revert "Do not allow spliting in res_pf, this is reserved for pretyping"Enrico Tassi
This reverts commit 8d8200d4bff3ffc44efc51ad44dccee9eb14ec6a. Fix #7936 # Conflicts: # proofs/clenvtac.ml
2018-11-07Merge PR #8918: Fix overlays on Windows CIMichael Soegtrop
2018-11-07[doc] nodes in ssr are monospaceEnrico Tassi
2018-11-07multi line comments don't have a titleEnrico Tassi
2018-11-07[doc] adapt comments in plugins/ssr/*.v to coqdoc styleEnrico Tassi
2018-11-07[doc] also scan plugins/ to build the lirbary indexEnrico Tassi
2018-11-07Merge PR #8868: [Docker] Update OCaml (4.07.1) and camlp5 (7.07-almost)Emilio Jesus Gallego Arias
2018-11-07Merge PR #8773: [checker] Refactor by sharing code with the kernelPierre-Marie Pédrot
2018-11-07Merge PR #8926: Move features that were not backported to 8.9 to the 8.10 ↵Guillaume Melquiond
section of CHANGES.md.
2018-11-06Fixes #8910 (typo in nameops.ml).Hugo Herbelin
[ci skip]
2018-11-06Optimise git cloningKamil Trzciński
2018-11-06Move features that were not backported to 8.9 to the 8.10 section of CHANGES.md.Théo Zimmermann
2018-11-06Merge PR #8889: Program hook gives back an obligation substitiutionPierre-Marie Pédrot
2018-11-06[dune] Add "quick" and "check" targets for fast builds.Emilio Jesus Gallego Arias
In #8900 a quicker build target is requested, this PR does provide targets towards that goal. - `check`, introduced in Dune 1.5.0, will build all ml files in a fast way, - `quick{byte,opt}`, does build a set of relevant hand-picked targets. Further improvements could come from having `coq_dune` use `coqtop.byte` when appropriate, taking advantage from https://github.com/ocaml/dune/issues/1073, and not generating rules for `.vo` files.
2018-11-06Update/improve two aspects of the merging process.Théo Zimmermann
Following discussion in #7042, we write down an advice to give time for last comments before merging potentially controversial PRs. We document a practice that is becoming standard in order to improve PR merging time: some other maintainer can self-assign if the main maintainer is not responding. Encourage component maintainers to announce when they won't be available. We document the practice of code owner teams. Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
2018-11-06[Docker] Update COMPILER_EDGE: 4.07.0 → 4.07.1Vincent Laporte
Also update CAMLP5_VER_EDGE: 7.06 → 7.06.10-g84ce6cc4 This is to avoid an OCaml bug that occurs when compiling the OCaml code extracted from part of a patched version of CompCert. ~~~ File "extraction/Parser.ml", line 12375, characters 19-29: Error: Constraints are not satisfied in this type. Type initstate' should be an instance of initstate' ~~~ This compiler issue only appears with OCaml 4.07.0 (neither with 4.06 nor with 4.07.1); hence this update.
2018-11-06Fix overlays on Windows CIGaëtan Gilbert
"${foo+}" is always the empty string "${foo-}" is "$foo" when foo is set and empty string when it's unset.
2018-11-06Bring back context printing in checkerMaxime Dénès
2018-11-06Checker now disables VM and nativeMaxime Dénès
At the same time, we made the safe_env threading explicit.
2018-11-06Remove checker files from .gitignoreMaxime Dénès
2018-11-06[checker] Check univ constraints induced by module subtypingMaxime Dénès
2018-11-06[checker] Fix "error related to inductive types"Maxime Dénès
2018-11-06[checker] Refactor by sharing code with the kernelMaxime Dénès
For historical reasons, the checker was duplicating a lot of code of the kernel. The main differences I found were bug fixes that had not been backported. With this patch, the checker uses the kernel as a library to serve the same purpose as before: validation of a `.vo` file, re-typechecking all definitions a posteriori. We also rename some files from the checker so that they don't clash with kernel files.
2018-11-06Move debug term printer to kernelMaxime Dénès
2018-11-06Merge PR #8912: [dune] [coqide] Use copy action instead of (run cp ...)Théo Zimmermann
2018-11-06Merge PR #8903: [dune] Add to vo rules explicit location of coqlib in boot mode.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 18:08:08 +0000