aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-23Merge PR #7567: Clean-up dead file in test-suite.Enrico Tassi
2018-05-22[ci] Build fiat-crypto targets in sequenceJason Gross
This should hopefully alleviate memory problems on gitlab, by first building the `lite` targets, and then building the remaining not-that-big targets.
2018-05-22Merge PR #7565: Document the new nested-proof error message.Emilio Jesus Gallego Arias
2018-05-22Merge PR #7577: Fixing debugger after #6859 (loading dynlink.cma before ↵Emilio Jesus Gallego Arias
lib.cma).
2018-05-22Mention warning and error message docs in PR templateJason Gross
This closes #7580 c.f. https://github.com/coq/coq/pull/7559#issuecomment-390749207 and https://github.com/coq/coq/pull/7559#issuecomment-390872924. This should be reverted if and when we move to autogenerated docs for warnings and errors, as suggested in #7373.
2018-05-22Fixing debugger after #6859 (loading dynlink.cma before lib.cma).Hugo Herbelin
2018-05-22[doc] Document the new report_undocumented_coq_objects settingClément Pit-Claudel
2018-05-22[doc] Add a list of common mistakesClément Pit-Claudel
2018-05-22[doc] Fix an incorrect use of $PWD in Makefile.docClément Pit-Claudel
2018-05-22[doc] Add a setting to warn about empty Coq objectsClément Pit-Claudel
2018-05-22Merge PR #7384: Split UniversesPierre-Marie Pédrot
2018-05-22Add myself as a secondary maintainer for the documentation.Théo Zimmermann
To reflect reality. [ci skip]
2018-05-22Merge PR #7324: Infrastructure for ocamldebug on the checkerHugo Herbelin
2018-05-22Merge PR #7526: [circle] Use Docker image from Gitlab registry.Gaëtan Gilbert
2018-05-22Merge PR #7568: [ci] [gitlab] Fix printenv sorting for variables that span ↵Gaëtan Gilbert
multiple lines
2018-05-22[build] Add -cclib -lcoqrun options to build of kernel.cmxa.Emilio Jesus Gallego Arias
It seems that it is standard practice in the OCaml world to set the `-cclib` flags at library creation time, at least in native libraries. Indeed, this seems to make linking easier as seen for example in #7563.
2018-05-22Merge PR #6859: [stm] Make toplevels standalone executables.Théo Zimmermann
2018-05-21Simplify the newring hack.Pierre-Marie Pédrot
The new implementation is 100% compatible with the previous one, but it is more compact and does not use a tricky translation function from the kernel.
2018-05-21[ci] [gitlab] Fix printenv sorting for variables that span multiple lines.Emilio Jesus Gallego Arias
2018-05-21Fix an anomaly when calling Obligation 0 or Obligation -1.Théo Zimmermann
I didn't change the parser which expects an integer instead of a positive number because changing it would also mean having worse error messages because of our current LL parser. The error message would have been: Syntax error: 'Tactic' ':=' expected after 'Obligation' (in [vernac:command]).
2018-05-21Remove a dead old-refman file.Théo Zimmermann
2018-05-21Document the new nested-proof error message.Théo Zimmermann
2018-05-21[ide] Remove special option `-ideslave`Emilio Jesus Gallego Arias
This has no effect anymore, verbose printing is controlled now by the regular, common `quiet` flag.
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
We turn coqtop "plugins" into standalone executables, which will be installed in `COQBIN` and located using the standard `PATH` mechanism. Using dynamic linking for `coqtop` customization didn't make a lot of sense, given that only one of such "plugins" could be loaded at a time. This cleans up some code and solves two problems: - `coqtop` needing to locate plugins, - dependency issues as plugins in `stm` depended on files in `toplevel`. In order to implement this, we do some minor cleanup of the toplevel API, making it functional, and implement uniform build rules. In particular: - `stm` and `toplevel` have become library-only directories, - a new directory, `topbin`, contains the new executables, - 4 new binaries have been introduced, for coqide and the stm. - we provide a common and cleaned up way to locate toplevels.
2018-05-21[ci] Add Dune to the base system.Emilio Jesus Gallego Arias
It is needed by Elpi and pidetop, and it is anyways needed for most OCaml packages, including some Coq tools in the future. The future base Docker image will include it by default.
2018-05-20Maitainers for components of the test-suite (closes #7426).Théo Zimmermann
[ci skip]
2018-05-20[codeowner] Add comment.Théo Zimmermann
[ci skip]
2018-05-20Make Pierre-Marie a secondary maintainer of the kernel and checker.Théo Zimmermann
[ci skip]
2018-05-20Merge PR #7557: Add test cases from #7554Théo Zimmermann
2018-05-20Add test cases from #7554Tej Chajed
Failed in v8.7.2 but were fixed by v8.8.0.
2018-05-19Merge PR #7527: [windows] Don't build menhir and int anymore in the ↵Michael Soegtrop
packaging scripts.
2018-05-18Merge PR #7550: [CI] Fix the script used by math-classes.Emilio Jesus Gallego Arias
2018-05-18Fix #7539: Checker does not properly handle negative coinductive types.Pierre-Marie Pédrot
The reduction machine of the checker was not taking into account the fact that cofixpoints needed to be unfolded when applied against a projection.
2018-05-18Merge PR #6965: [api] Move universe syntax to `Glob_term`Pierre-Marie Pédrot
2018-05-18Clean-up dead file in test-suite.Théo Zimmermann
2018-05-18Create a documentation for the release manager.Théo Zimmermann
This process is expected to evolve in the future as we automate it more and more. [ci skip]
2018-05-18[CI] Fix the script used by math-classes.Pierre-Marie Pédrot
We call configure to properly regenerate the Makefile and its dependencies.
2018-05-17Split off Universes functions for minimization.Gaëtan Gilbert
This finishes the splitting of Universes.
2018-05-17Make Universes.refresh_constraints internal to UStateGaëtan Gilbert
2018-05-17Split off Universes functions about substitutions and constraintsGaëtan Gilbert
2018-05-17Remove unused argument to solve_constraints_systemGaëtan Gilbert
2018-05-17Move solve_constraint_system near its only use site (comInductive)Gaëtan Gilbert
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert
This API is a bit strange, I expect it will change at some point.
2018-05-17Stop using Universes.subst(_opt)_univs_constrGaëtan Gilbert
Should it be removed? The underlying `universe_subst -> constr -> constr` seems like it could be useful for plugins but where would the substitution be from?
2018-05-17Make set minimization option internal to UniversesGaëtan Gilbert
2018-05-17[circle] Use Docker image from Gitlab registry.Emilio Jesus Gallego Arias
2018-05-17Merge PR #7451: Introduce an option to allow nested lemma, and turn it off ↵Emilio Jesus Gallego Arias
by default.
2018-05-17Merge PR #7359: Reduce usage of evar_map referencesPierre-Marie Pédrot
2018-05-17Merge PR #7449: [vernac] taint two out-of-api `to_constr` use in ↵Pierre-Marie Pédrot
`comDefinition`.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 01:44:29 +0000