aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-05-07Add CODEOWNERS entry for check-owners*.shGaëtan Gilbert
2018-05-07Merge PR #7347: Fix for #7081 (Windows lablgtk) and #7083 (Windows logging)Maxime Dénès
2018-05-07Merge PR #7371: Propose some updates of the CODEOWNER file.Maxime Dénès
2018-05-07Merge PR #7445: [ci] Add ounit to the base Docker package set.Gaëtan Gilbert
2018-05-07Merge PR #7301: [sphinx] Backport forgotten updates during the migration & ↵Maxime Dénès
other improvements
2018-05-07Merge PR #7440: [ci] Add a default target to `Makefile.ci`Gaëtan Gilbert
2018-05-07[ci] Add ounit to the base Docker package set.Emilio Jesus Gallego Arias
This should help #6808.
2018-05-07Merge PR #7427: Fix #7413: coqdep warning on repeated filesPierre-Marie Pédrot
2018-05-06Merge PR #7387: [gitlab] [circleci] Use a Docker base image for CIGaëtan Gilbert
2018-05-06Merge PR #6156: [api] Rename `global_reference` to `GlobRef.t` to follow ↵Maxime Dénès
kernel style.
2018-05-06[ci] Add a default target to `Makefile.ci`Emilio Jesus Gallego Arias
So we avoid problems like the one in #7438.
2018-05-05[gitlab] [circleci] Use a Custom Docker Image as base CI setup.Emilio Jesus Gallego Arias
We provide a custom `Dockerfile` for Coq's CI system, based on `ubuntu:bionic`. The image includes the required set of packages and OPAM switches. This greatly simplifies the Gitlab and Circle scripts, at the cost of having to push a Docker build for them to depend on. Travis is not included in this PR as it requires significant more refactoring due to lack of native Docker support. This is work in progress but ready, a build hook is used so the image is properly tagged in the Docker autobuilder. We need to improve the autobuilder setup but this last point requires some design on how to trigger it. Fixes #7383
2018-05-05[sphinx] Fixes around apply, including indentation and fixing a Coq warning.Théo Zimmermann
2018-05-05[sphinx] Fixes around refine, including indentation and a hard-coded ref.Théo Zimmermann
2018-05-05[sphinx] Improve typeclass chapter.Théo Zimmermann
2018-05-05[sphinx] Add indices for only, all and par.Théo Zimmermann
2018-05-05[sphinx] Improvements around injection tactic.Théo Zimmermann
2018-05-05[sphinx] Improve part about Hints.Théo Zimmermann
Fix Hint (Transparent | Opaque) index.
2018-05-05[sphinx] Re-indent to get much better rendering.Théo Zimmermann
Add some more cmd references. And use deprecated directives.
2018-05-05Remove duplicate Introduction title.Théo Zimmermann
2018-05-05[sphinx] Backport changes from #5979.Théo Zimmermann
2018-05-05Two more uses of verbatim in doc.Théo Zimmermann
2018-05-05Clean-up around cmd documentation.Théo Zimmermann
In particular, remove trailing dots.
2018-05-05Remove duplicate Extraction commands documentation.Théo Zimmermann
2018-05-05Add some refs in the Omega chapter.Théo Zimmermann
2018-05-05More fixes in the Generalized Rewriting chapter.Théo Zimmermann
2018-05-05[sphinx] Replace remaining `@natural` by `@num`.Théo Zimmermann
2018-05-05[sphinx] More use of cmd references in Extraction chapter.Théo Zimmermann
2018-05-05[sphinx] Use references for command Info.Théo Zimmermann
2018-05-05[sphinx] More reference fixes.Théo Zimmermann
2018-05-05[sphinx] Fix a porting mistake.Théo Zimmermann
2018-05-05[sphinx] Use references for Print.Théo Zimmermann
2018-05-05Fix error messages and make them consistent.Théo Zimmermann
All the error messages start with a capitalized letter and end with a dot.
2018-05-05Add direct reference to congruence with.Théo Zimmermann
2018-05-05Clean-up around options.Théo Zimmermann
- Remove all trailing dots. - There is only one Bullet Behavior option. - Replaces `@natural` and `@integer` by `@num`.
2018-05-05debug trivial and debug auto were not in the tactic index.Théo Zimmermann
2018-05-05Fix failing example in refman.Théo Zimmermann
2018-05-05[sphinx] Fix some references.Théo Zimmermann
2018-05-05[sphinx] Use option direct reference.Théo Zimmermann
2018-05-05[sphinx] Fix a typo that appeared during the migration.Théo Zimmermann
2018-05-05[sphinx] Fix a hardcoded reference.Théo Zimmermann
2018-05-05[sphinx] Backport reformulation.Théo Zimmermann
(cf. 711b9d8cdf6e25690d247d9e8c49f005527e64e2)
2018-05-05[sphinx] Backport fix of typo.Théo Zimmermann
(cf. 6131f89f6b91c45e641dd877df8719fa77987453)
2018-05-05Fix typo in Coercions chapter.Théo Zimmermann
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at.
2018-05-04Merge PR #7416: Fix #7415. Printing Width was not applied to error messages.Emilio Jesus Gallego Arias
2018-05-04Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.Pierre-Marie Pédrot
2018-05-04Fix #7413: coqdep warning on repeated filesGaëtan Gilbert
The same warning exists in ocamllibdep so I copied the change there. Detecting when 2 paths are the same is approximate, eg ././a.ml and a.ml are considered different. Implementing realpath probably isn't worth doing for this warning.
2018-05-03Merge PR #7134: When an error comes from loading the prelude, tell it ↵Emilio Jesus Gallego Arias
happened at initialization time
2018-05-03Merge PR #7375: Implement to_constr with nf_evars_and_universes_opt_substPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 06:51:03 +0000