aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* [gitlab] Add bleeding-edge flambda build.Gravatar Emilio Jesus Gallego Arias2018-05-07
| | | | | | | | | | | | | | We also introduce a bit more systematic job naming: `base/edge`. In order to make the flambda switch selectable we update the Docker image so all the dependencies are installed in that one. Note the extra quote rule for the flambda parameters, but unless we can assign arrays to Gitlab variables there is not a good way to do this I'm afraid. With this patch we are getting close to being able to remove most builds from Travis.
* Merge PR #7445: [ci] Add ounit to the base Docker package set.Gravatar Gaëtan Gilbert2018-05-07
|\
* \ Merge PR #7301: [sphinx] Backport forgotten updates during the migration & ↵Gravatar Maxime Dénès2018-05-07
|\ \ | | | | | | | | | other improvements
* \ \ Merge PR #7440: [ci] Add a default target to `Makefile.ci`Gravatar Gaëtan Gilbert2018-05-07
|\ \ \
| | | * [ci] Add ounit to the base Docker package set.Gravatar Emilio Jesus Gallego Arias2018-05-07
| | | | | | | | | | | | | | | | This should help #6808.
* | | | Merge PR #7427: Fix #7413: coqdep warning on repeated filesGravatar Pierre-Marie Pédrot2018-05-07
|\ \ \ \ | |_|_|/ |/| | |
* | | | Merge PR #7387: [gitlab] [circleci] Use a Docker base image for CIGravatar Gaëtan Gilbert2018-05-06
|\ \ \ \
* \ \ \ \ Merge PR #6156: [api] Rename `global_reference` to `GlobRef.t` to follow ↵Gravatar Maxime Dénès2018-05-06
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | kernel style.
| | | | * | [ci] Add a default target to `Makefile.ci`Gravatar Emilio Jesus Gallego Arias2018-05-06
| |_|_|/ / |/| | | | | | | | | | | | | | So we avoid problems like the one in #7438.
| | * | | [gitlab] [circleci] Use a Custom Docker Image as base CI setup.Gravatar Emilio Jesus Gallego Arias2018-05-05
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| | | * [sphinx] Fixes around apply, including indentation and fixing a Coq warning.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] Fixes around refine, including indentation and a hard-coded ref.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] Improve typeclass chapter.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] Add indices for only, all and par.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] Improvements around injection tactic.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] Improve part about Hints.Gravatar Théo Zimmermann2018-05-05
| | | | | | | | | | | | | | | | Fix Hint (Transparent | Opaque) index.
| | | * [sphinx] Re-indent to get much better rendering.Gravatar Théo Zimmermann2018-05-05
| | | | | | | | | | | | | | | | | | | | Add some more cmd references. And use deprecated directives.
| | | * Remove duplicate Introduction title.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] Backport changes from #5979.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * Two more uses of verbatim in doc.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * Clean-up around cmd documentation.Gravatar Théo Zimmermann2018-05-05
| | | | | | | | | | | | | | | | In particular, remove trailing dots.
| | | * Remove duplicate Extraction commands documentation.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * Add some refs in the Omega chapter.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * More fixes in the Generalized Rewriting chapter.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] Replace remaining `@natural` by `@num`.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] More use of cmd references in Extraction chapter.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] Use references for command Info.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] More reference fixes.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] Fix a porting mistake.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] Use references for Print.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * Fix error messages and make them consistent.Gravatar Théo Zimmermann2018-05-05
| | | | | | | | | | | | | | | | All the error messages start with a capitalized letter and end with a dot.
| | | * Add direct reference to congruence with.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * Clean-up around options.Gravatar Théo Zimmermann2018-05-05
| | | | | | | | | | | | | | | | | | | | | | | | - Remove all trailing dots. - There is only one Bullet Behavior option. - Replaces `@natural` and `@integer` by `@num`.
| | | * debug trivial and debug auto were not in the tactic index.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * Fix failing example in refman.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] Fix some references.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] Use option direct reference.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] Fix a typo that appeared during the migration.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] Fix a hardcoded reference.Gravatar Théo Zimmermann2018-05-05
| | | |
| | | * [sphinx] Backport reformulation.Gravatar Théo Zimmermann2018-05-05
| | | | | | | | | | | | | | | | (cf. 711b9d8cdf6e25690d247d9e8c49f005527e64e2)
| | | * [sphinx] Backport fix of typo.Gravatar Théo Zimmermann2018-05-05
| | | | | | | | | | | | | | | | (cf. 6131f89f6b91c45e641dd877df8719fa77987453)
| | | * Fix typo in Coercions chapter.Gravatar Théo Zimmermann2018-05-05
| |_|/ |/| |
| * | [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | Merge PR #7416: Fix #7415. Printing Width was not applied to error messages.Gravatar Emilio Jesus Gallego Arias2018-05-04
|\ \ \ | |/ / |/| |
* | | Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.Gravatar Pierre-Marie Pédrot2018-05-04
|\ \ \
| | | * Fix #7413: coqdep warning on repeated filesGravatar Gaëtan Gilbert2018-05-04
| |_|/ |/| | | | | | | | | | | | | | | | | | | | 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.
* | | Merge PR #7134: When an error comes from loading the prelude, tell it ↵Gravatar Emilio Jesus Gallego Arias2018-05-03
|\ \ \ | | | | | | | | | | | | happened at initialization time
* \ \ \ Merge PR #7375: Implement to_constr with nf_evars_and_universes_opt_substGravatar Pierre-Marie Pédrot2018-05-03
|\ \ \ \
| | | | * Fix #7415. Printing Width was not applied to error messages.Gravatar Pierre Courtieu2018-05-03
| | | | |
* | | | | Merge PR #7304: Make `intro`/`intros` progress on existential variables.Gravatar Pierre-Marie Pédrot2018-05-03
|\ \ \ \ \ | |_|_|_|/ |/| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 19:18:59 +0000