aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-03-13Deprecation of catchable_exception, to be replaced by noncritical in try-with.Hugo Herbelin
2020-03-13Removing catchable_exception test in tclOR/tclORELSE.Hugo Herbelin
Since tclOR/tclORELSE are not supposed to return critical exceptions, we don't need to replace catchable_exception by noncritical.
2020-03-13Replacing catchable_exception by noncritical in try-with blocks.Hugo Herbelin
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-12Update doc/sphinx/addendum/extended-pattern-matching.rstlarsr
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-03-12Fixed link to "match" syntax. larsr
and removed the now incorrect "section 8.2.3" reference, as it is the same as the "refine" link.
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-12Documenting when exceptions are noncritical in the proof engineHugo Herbelin
2020-03-12Add changelogSimonBoulier
2020-03-12Add message at the end of search results about implicit argumentsSimonBoulier
2020-03-12Print implicit arguments in types of referencesSimonBoulier
2020-03-12Dune build rules for doc_grammar and fullGrammar.Théo Zimmermann
2020-03-12Add changelog entrySimonBoulier
2020-03-12Remove a positivity check when Check Positivity is offSimonBoulier
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-11Comment difference between the 2 hashes on constrGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 08:55:38 +0000