aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-06-09Merge PR #7515: gitlab: build sphinx doc in separate jobEmilio Jesus Gallego Arias
2018-06-09Merge PR #7642: Gitlab: retry failed jobs onceEmilio Jesus Gallego Arias
2018-06-08gitlab: build sphinx doc in separate jobGaëtan Gilbert
2018-06-08Existing Class noop when already a class + warning.Gaëtan Gilbert
Fix #5012.
2018-06-08Merge PR #7739: add test for #7595Gaëtan Gilbert
2018-06-08Merge PR #7747: dev/doc/univpoly.{txt => md}, split off primitive projection ↵Théo Zimmermann
info
2018-06-08Add a bit of doc to EConstr.decompose_lam*Gaëtan Gilbert
2018-06-08[doc] Disable smartquotes conversionClément Pit-Claudel
Closes GH-7742.
2018-06-08dev/doc/univpoly.{txt => md}, split off primitive projection infoGaëtan Gilbert
2018-06-08Gitlab: retry failed "build" jobs onceGaëtan Gilbert
2018-06-08Merge PR #7417: Micromega clean-upThéo Zimmermann
2018-06-08Merge PR #7687: [ci] [docker] Pin specific versions of OPAM CI dependencies.Gaëtan Gilbert
2018-06-07Micromega clean-upMaxime Dénès
We add .mli files, removed dead code and use standard combinators instead of redefined ad-hoc ones in a few places. A lot of cleaning still has to be done on this code: documenting the interfaces, resolving the many abstraction leaks. I suspect there is still a lot of code duplication.
2018-06-07add test for #7595Ralf Jung
2018-06-07Merge PR #7735: Remove cross-crypto from Travis. It is still tested in ↵Emilio Jesus Gallego Arias
GitLab CI.
2018-06-07Remove cross-crypto from Travis. It is still tested in GitLab CI.Théo Zimmermann
This fixes #7734.
2018-06-07Fix the checker by merely adapting the data structure.Pierre-Marie Pédrot
Unluckily, this is completely wrong as we trust the inlined term to be well-typed in some unavailable environment. To start with, the checker should not even rely on substitutions as it does not trust functors, but it does anyways. I have thus commented this code as a useful backdoor for when Coq is used to implement the next blockchain Ponzi scheme. We really need to sort this out though.
2018-06-07Fix #7615: Functor inlining drops universe substitution.Pierre-Marie Pédrot
We store the universe context in the inlined terms and apply it to the instance provided to the substitution function. Technically the context is not needed, but we use it to assert that the length of the instance corresponds, just in case.
2018-06-07Merge PR #7629: Fix anomaly in autoapply when an unbound hint name is providedMatthieu Sozeau
2018-06-07Merge PR #7706: Fix wrong deprecation msgPierre-Marie Pédrot
2018-06-07Merge PR #6874: [econstr] Some minor tweaksPierre-Marie Pédrot
2018-06-06Merge PR #7721: Add a note about [ci skip] in CI README.Emilio Jesus Gallego Arias
2018-06-06[ci] [docker] Pin specific versions of OPAM CI dependencies.Emilio Jesus Gallego Arias
Packages such as `menhir` or `elpi` are fragile w.r.t. updates, so allowing a non-deterministic install in the Dockefile seems risky. We have found trouble with Menhir in the past. We thus specify a concrete version for all `CI_OPAM` packages. cc: https://github.com/AbsInt/CompCert/issues/234 We also add remove `hevea` from `apt` dependencies as it hasn't been needed since #7466 and add `texlive-science` which is needed to build the `source-doc` target due to the `textgreek` package being used.
2018-06-06Add a note about [ci skip] in CI README.Théo Zimmermann
2018-06-06Merge PR #7717: [ci] Temporal fix for CompCertGaëtan Gilbert
2018-06-06[ci] Temporal fix for CompCertEmilio Jesus Gallego Arias
https://github.com/AbsInt/CompCert/issues/234
2018-06-05Merge PR #7679: Clean native compilation of primitive projectionsMaxime Dénès
2018-06-05Merge PR #7004: Make `simple apply` obey `Opaque` directive.Pierre-Marie Pédrot
2018-06-05Merge PR #7077: Preserving canonical structure of return predicate in ↵Maxime Dénès
vm_compute and native_compute (partial fix to #7068; also fixes #7076))
2018-06-05Merge PR #7663: test suite: make target to regenerate failing output testsEnrico Tassi
2018-06-05Improve links to SSR tactics, and some other improvements.Théo Zimmermann
2018-06-05Merge PR #7464: Make whitespace linter not check for trailing space.Maxime Dénès
2018-06-05Define rec_declaration in terms of prec_declaration.SimonBoulier
And similarly for fixpoint and cofixpoint.
2018-06-05Update evarutil.mliMatthieu Sozeau
Actually all the new_ functions are in evarutil still
2018-06-05Fix wrong deprecation msgMatthieu Sozeau
2018-06-05Workaround a weird error of .. coqtop::Théo Zimmermann
2018-06-05Remove many abusive .. coqtop in SSR chapter.Théo Zimmermann
Many still remain.
2018-06-05A few additional small fixes.Théo Zimmermann
2018-06-05[sphinx] Fix missing indices warnings.Théo Zimmermann
2018-06-05[ssr] index entry for "without loss", "suffices" and "generally have"Enrico Tassi
2018-06-05[ssr] some fixes to the documentation markupEnrico Tassi
2018-06-05[sphinx] Start fixing SSR chapter.Théo Zimmermann
2018-06-05More straightforward native compilation of primitive projections.Pierre-Marie Pédrot
Instead of having a constant-based compilation of projections, we generate them at the compilation time of the inductive block to which they pertain.
2018-06-05Use projection indices in native compilation rather than constant names.Pierre-Marie Pédrot
2018-06-05Merge PR #7643: Fix #7631: native_compute fails to compile an example in Coq 8.8Pierre-Marie Pédrot
2018-06-05Merge PR #7690: Fixing typos in file Berardi.vPierre-Marie Pédrot
2018-06-05Merge PR #7646: Fix #4714: Stack overflow with native computePierre-Marie Pédrot
2018-06-05Merge PR #7099: Stronger invariants in unification signature.Matthieu Sozeau
2018-06-05Merge PR #7453: Refuse to parse empty [Context] command.Matthieu Sozeau
2018-06-05Merge PR #7495: Fix restrict_universe_contextMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 01:26:35 +0000