aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-09-24Merge PR #8530: Fix typo in comment.Hugo Herbelin
2018-09-24Merge PR #8536: Fix #8513: EConstr.eq_constr doesn't properly take into ↵Gaëtan Gilbert
account universe variables
2018-09-24Merge PR #8537: [default.nix] Bump nixpkgs to use Dune 1.2.1.Vincent Laporte
2018-09-24Merge PR #8519: Issue #8514 windows ci failuresThéo Zimmermann
2018-09-23[default.nix] Bump nixpkgs to use Dune 1.2.1.Théo Zimmermann
2018-09-23Fix #8513: EConstr.eq_constr doesn't properly take into account universe ↵Pierre-Marie Pédrot
variables. We simply normalize the universe variables before comparing them.
2018-09-23Merge PR #8465: Small cleanup of summary usesPierre-Marie Pédrot
2018-09-23Merge PR #8247: Show diffs on multiple changed goals; match old and new goal ↵Emilio Jesus Gallego Arias
info
2018-09-22Fix typo in comment.Nick Lewycky
2018-09-21Merge PR #8500: [api] Deprecate two forgotten print functions that use ↵Hugo Herbelin
global state.
2018-09-21Merge PR #8526: Fix Travis CI by pinning brew OPAM package to version 1.2.2.Gaëtan Gilbert
2018-09-21Fix Travis CI by pinning brew OPAM package to version 1.2.2.Théo Zimmermann
2018-09-21Merge PR #8522: [dune] Improve support for Coq tools.Théo Zimmermann
2018-09-21Merge PR #8516: CHANGES for 8.8.2.Théo Zimmermann
2018-09-21[dune] Improve support for Coq tools.Emilio Jesus Gallego Arias
- Install `CoqMakefile.in` - Build `coqwc` and `coqdoc` This allows to build most contribs I've tried with the Dune-based OPAM package.
2018-09-21Merge pull request #8462 from vbgl/zify-colonequalLaurent Théry
Zify: replace local definitions by equations
2018-09-21Merge PR #8443: [opam] [dune] Fix typo + set prefix for configure.Théo Zimmermann
2018-09-21Merge PR #8521: Create a team of micromega maintainersThéo Zimmermann
2018-09-21Create a team of micromega maintainersMaxime Dénès
2018-09-21Use unique names in windows CI for cygwin and coq install folderMichael Soegtrop
Don't zip artifacts but create an artifact folder structure
2018-09-21Merge PR #8439: Update documentation of options and flagsThéo Zimmermann
2018-09-21Merge PR #8455: Move tests in bugs/ to bugs/closed/.Théo Zimmermann
2018-09-21Merge commit 6a8c37c02504463afaa677641d75d9977020edf6 Windows buildfile ↵Michael Soegtrop
cleanup and stability and logging enhancements from v8.8
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
Mark boolean-valued options with :flag: Adjust tactic and command names so parameters aren't shown in the index unless they're needed for disambiguation. Remove references to synchronous options. Revise doc for tables. Correct indentation for text below :flag:
2018-09-21[dune] [configure] Allow to set prefix using environment variable.Emilio Jesus Gallego Arias
This is a hack to enable correct OPAM building, the medium-term plan is to avoid having to set a prefix at configure time but instead using a set of rules to locate the Coq library. We use `(env_var ...)` in a dependency rule, which a feature of Dune 1.2
2018-09-21Merge PR #8518: [dune] Add "watch" target for continuous build mode.Théo Zimmermann
2018-09-20[dune] Add "watch" target for continuous build mode.Emilio Jesus Gallego Arias
`make -f Makefile.dune watch` will now watch for files changes and rebuild what is needed. This feature requires `fswatch` or `inotifywait`, and Dune >= 1.2.0. Note that the current CI image ships an older Dune version.
2018-09-20Define flags (binary-valued settings) and tables (settings that are sets)Jim Fehrle
as separate NotationObject types, include in index.
2018-09-20CHANGES for 8.8.2.Théo Zimmermann
2018-09-20Current diff code only compares the first current goal of the old and newJim Fehrle
proof states. That's not always correct. This change will a) show diffs for all displayed goals and b) correctly match goals between the old and new proof states. For example, "split." will show diffs for both resulting goals. "all: swap 1 2" will show the same diffs as for the old proof state, though in a different position in the output. Please see comments before Proof_diffs.make_goal_map_i and Proof_diffs.match_goals for a description of how goals are matched between old and new proofs.
2018-09-20[opam] Fix typo in build variable.Emilio Jesus Gallego Arias
Fixes #8431
2018-09-20Merge PR #8418: Add a PDF version of the manualThéo Zimmermann
2018-09-20Merge PR #8297: Fix #7754: universe declarations on mutual inductivesMatthieu Sozeau
2018-09-20Stop building LaTeX doc in Travis (keep HTML).Théo Zimmermann
The LaTeX doc is already tested in GitLab CI and finding the right dependencies in this older version of Ubuntu is a hurdle.
2018-09-20Mention PDF doc in CHANGES.Théo Zimmermann
2018-09-20Fix race condition.Théo Zimmermann
2018-09-20Update minimum required dependency versions of Sphinx doc.Théo Zimmermann
The minimum required versions of the Sphinx-related (and ANTLR) Python packages for Coq 8.10 were chosen as the lower bound between what is currently in Debian Buster and in NixOS 18.09 Jellyfish (in practice the lower bound was always met by NixOS 18.09 Jellyfish). These minimum required versions were documented. In the docker image used by GitLab CI, we install these Python packages through pip as this allows us to pin them to these specific versions. In Travis, we let them unspecified to always test the latest versions. Finally, we also add the new dependencies of the Sphinx PDF manual.
2018-09-20[doc] Replace app.info (deprecated in Sphinx 8.0) with logger.infoClément Pit-Claudel
2018-09-20[doc] Remove unneeded backslashes in biblio.bibClément Pit-Claudel
2018-09-20[doc] Skip unneeded copies in copy_formatspecific_filesClément Pit-Claudel
2018-09-20[doc] Move a citation back into the introductionClément Pit-Claudel
Alternatively, we could duplicate the citation text in both index files.
2018-09-20[doc] Add sphinx-html, sphinx-latex, and sphinx-pdf targetsClément Pit-Claudel
2018-09-20[doc] Remove frames around code snippets in the LateX buildClément Pit-Claudel
2018-09-20[doc] Change the name that appears on the first page of the PDF manualClément Pit-Claudel
2018-09-20[doc] Fix some Sphinx LaTeX warnings and silence othersClément Pit-Claudel
2018-09-20[doc] Add another common mistake to the documentation-writing guideClément Pit-Claudel
2018-09-20[doc] Fix a few syntax highlighting issuesClément Pit-Claudel
2018-09-20[doc] Get rid of two Sphinx warningsClément Pit-Claudel
2018-09-20[doc] Fix more duplicate-label issues in production listsClément Pit-Claudel
2018-09-20[doc] Rewrite and document the prodn directiveClément Pit-Claudel
It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 03:24:57 +0000