aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-11-09Fix -top for univbinders output test.Gaëtan Gilbert
It was good enough for the makefile but not for emacs.
2018-11-09Merge PR #8601: Move bound universe names to abstract contextsGaëtan Gilbert
2018-11-09Add .cmt and generated ml files to gitignoreGaëtan Gilbert
2018-11-09Adapt to coq/coq#8933 (Make initial evar map argument to ↵Gaëtan Gilbert
check_evars_are_solved optional)
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-09Fix dune runtest invocationGaëtan Gilbert
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-09[topfmt] Add phase attribute for toplevel printing.Emilio Jesus Gallego Arias
This is localized version of #8833, but instead of adding a phase attribute which, as pointed by @gares has some problematic semantics, we add a local one to the toplevel functions. This moves the imperative part of the API to a better-delimited scope and allows to progress with the separation of the interactive and compilation API. Note that still quite a few issues do remain in the "Feedback" path, for example, idetop and other feedback clients cannot get a hold of the feedback early enough as to direct init messages to the IDE part. This is for example a serious issue of the API that shall be treated separately.
2018-11-09Merge PR #8947: Ensure termination of `file_exists_respecting_case`Emilio Jesus Gallego Arias
2018-11-08[dune] Some tweaks to docs.Emilio Jesus Gallego Arias
2018-11-08Remove checker printersGaëtan Gilbert
Now that the checker is using the regular kernel files it can also use the normal printers.
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-08[VM] Fix compilation of int31 eliminatorsVincent Laporte
The compilation to bytecode of the elimination schemes for int31 must happen after the int31 type is registered to the retroknowledge. Otherwise, the “decompint” instruction is not emitted.
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-07[Funind plugin] Remove some dead codeVincent Laporte
2018-11-07[Firstorder plugin] Remove some dead codeVincent Laporte
2018-11-07[CC plugin] Remove dead codeVincent Laporte
2018-11-07[R syntax plugin] Remove some dead codeVincent Laporte
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-07Merge pull request #17 from ejgallego/fix_warnYves Bertot
[warnings] Fix couple of warnings related to API..
2018-11-07[warnings] Fix couple of warnings related to API..Emilio Jesus Gallego Arias
Changes in declare following @SkySkimmer's advice.
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-07Merge pull request #16 from ejgallego/dunerizeYves Bertot
[dune] Add support for building with Dune for the ML part.
2018-11-07Merge pull request #15 from ejgallego/add_travisYves Bertot
[travis] Add Travis File.
2018-11-07[dune] Add support for building with Dune for the ML part.Emilio Jesus Gallego Arias
This allows to drop the plugin_tutorials in the coq tree and have the build compose.
2018-11-06Fixes #8910 (typo in nameops.ml).Hugo Herbelin
[ci skip]
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-01 23:22:19 +0000