aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-03-13Merge PR #11805: Fix coqchk for primitive integers on 32bit arch with OCaml ↵Pierre-Marie Pédrot
>= 4.08 (#11624) Reviewed-by: ppedrot
2020-03-13Merge PR #11016: [proof] Remove duplication in the proof save path.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: herbelin
2020-03-13Merge PR #11804: [CI] test hierarchy builder as part of elpiGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-13Merge PR #11815: [ci] [doc] Point to actual docker instructions.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-13Merge PR #11003: [vernac] Remove deprecated function.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-13[lemmas] Consolidate some declaration data on Info.tEmilio Jesus Gallego Arias
Now that `MutualEntry` provides a more uniform interface we can reuse `Info.t` In the medium term we shall consolidate `Proof` / `Proof_global` and `Lemmas` so admitted / finish are uniform too.
2020-03-12[declare] Remove trivial wrapperEmilio Jesus Gallego Arias
In preparation for the introduction of an opaque mutual definition type at the `Declare` level we remove the not very useful wrapper `declare_fix`. Now we should be ready to profit from `DeclareDef` and its handling of common stuff such as `restrict_universe_context` and `check_univ_decl` etc...
2020-03-12[lemmas] Handle mutual lemmas more uniformly.Emilio Jesus Gallego Arias
We split the paths for mutual / non-mutual constants, and we enforce some further invariants, in particular we avoid messing around with the body of saved constants, and using the indirect accessor. This should be almost semantically equivalent to the previous code, including some questionable choices present there. In further cleanups we will move this code to Declare, which should hopefully help clarify some of the semantics.
2020-03-12[save proof] Declare universe_binders unconditionally for mutual assumptions.Emilio Jesus Gallego Arias
As suggested by Gaëtan in review, we move declaration of universe binders to the common code in `DeclareDef`; this changes the semantics for the assumption case when Recthms is not empty.
2020-03-12[proof] Remove duplication in the proof save path.Emilio Jesus Gallego Arias
We move towards more unification in the proof save path of interactive and non-interactive proofs.
2020-03-12[vernac] Minor cleanup of opens in `Vernacentries`Emilio Jesus Gallego Arias
2020-03-12Merge PR #11796: Remove parallel building of Sphinx documentation.Emilio Jesus Gallego Arias
2020-03-12[ci] [doc] Point to actual docker instructions.Emilio Jesus Gallego Arias
2020-03-12Merge PR #11798: Tests make bytecodeEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: gares
2020-03-12Merge PR #11781: Minor improvements to the unreleased changelog.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2020-03-12Merge PR #11780: Minor improvements to the unreleased changelog.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2020-03-12Merge PR #11810: [dune] Fix ocamlopt_flags for release profileThéo Zimmermann
Reviewed-by: Zimmi48
2020-03-12[dune] Fix ocamlopt_flags for release profileEmilio Jesus Gallego Arias
Closes #11758 It turns out that we were overwriting the default `ocamlopt_flags`, thus creating a problem in the release build.
2020-03-11Merge PR #11754: [micromega] Add numerical compatibility layer.Frédéric Besson
Ack-by: SkySkimmer Reviewed-by: fajb
2020-03-11Merge PR #11800: [ci] [gitlab] Move VST to `allow_failure`Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-11Update dev/ci/ci-basic-overlay.shEnrico Tassi
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-03-11Fix coqchk for primitive integers on 32bit arch with OCaml >= 4.08 (#11624)Pierre Roux
2020-03-11[CI] test hierarchy builder as part of elpiEnrico Tassi
2020-03-11Merge PR #11769: Fix #9930: "change" replaces 0-param projections by constantsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-11Merge PR #11786: Fix #11730: Mangle Names vs InfixPierre-Marie Pédrot
Reviewed-by: herbelin Reviewed-by: ppedrot
2020-03-11Merge PR #11790: [lib] [ccalgo] Remove unused code / cleanupPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-10[ci] [gitlab] Move VST to `allow_failure`Emilio Jesus Gallego Arias
VST has been broken for a few days, moving to allow failure.
2020-03-10Merge PR #11767: Fix #11738 : Funind using deprecated Coqlib API.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: maximedenes
2020-03-10test coq-makefile/findlib-package-unpacked: only try to invoke 'make' whenRalf Treinen
there is an ocamlopt compiler.
2020-03-10test coq-makefile/camldep: try to build a cmx only when there is an ocamloptRalf Treinen
compiler. In any case, try to build a cmo file.
2020-03-10Merge PR #11788: Prevent CoqIDE from hanging when invalid channels are still ↵Michael Soegtrop
open. Reviewed-by: MSoegtropIMC
2020-03-10Remove parallel building of Sphinx documentation.Théo Zimmermann
Since version 1.0.0 of the sphinxcontrib-bibtex extension, parallel building of the Sphinx documentation emits a warning (and thus makes our warning-free build fail). This change was already done in Makefile.doc as part of #11732.
2020-03-10Merge PR #11732: Update the OCaml version in `default.nix` to 4.09.0Théo Zimmermann
Reviewed-by: Zimmi48
2020-03-10Merge PR #11764: Simplify mutual template polymorphismGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-10Merge PR #11763: Fixing an amusing small bug in parsing decimal numbers in RPierre-Marie Pédrot
Reviewed-by: ppedrot Reviewed-by: proux01
2020-03-10Fixing little bug in parsing decimal numbers in R.Hugo Herbelin
2020-03-10Disable parallel build of Sphinx documentationMaxime Dénès
We are using some Sphinx extensions that are not safe w.r.t. parallel reaading.
2020-03-10[plugins] [cc] Remove unused exports / mli file cleanup.Emilio Jesus Gallego Arias
2020-03-10[clib] Remove module CStackEmilio Jesus Gallego Arias
This is only used in `Ccalgo` and it does not provide any advantage these days over the upstream OCaml implementation.
2020-03-10Merge PR #11774: [exn] [nit] Remove not very useful re-raises.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-09Merge PR #11787: Do not erase OCAMLPATH in CI targets with Dune-built CoqEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-03-09Merge PR #11720: Remove some productionlistsThéo Zimmermann
Ack-by: Zimmi48
2020-03-09Remove some productionlistsJim Fehrle
2020-03-09Merge PR #11773: [doc] [dune] Update Dune build instructionsThéo Zimmermann
Reviewed-by: Zimmi48
2020-03-09Prevent CoqIDE from hanging when invalid channels are still open.Pierre-Marie Pédrot
This behaviour happens as a sub-bug of #10169 for instance.
2020-03-09Do not erase OCAMLPATH in CI targets with Dune-built CoqMaxime Dénès
2020-03-09Fix #11730: Mangle Names vs InfixGaëtan Gilbert
2020-03-09Fix #9930: "change" replaces 0-param projections by constantsGaëtan Gilbert
2020-03-09Add CI overlays.Pierre-Marie Pédrot
2020-03-08Ensure that template parameters are shared in the same inductive block.Pierre-Marie Pédrot
This could have been at the root of strange behaviours (read unsoundness).
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 09:18:45 +0000