aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-10Merge PR #11767: Fix #11738 : Funind using deprecated Coqlib API.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: maximedenes
2020-03-10Merge PR #11788: Prevent CoqIDE from hanging when invalid channels are still ↵Michael Soegtrop
open. Reviewed-by: MSoegtropIMC
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-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).
2020-03-08Template polymorphism is now a property of the inductive block.Pierre-Marie Pédrot
For an inductive block to be template, all its components must also be. This is probably fixing a few soundness bugs in the process, but I do not want to think too much about it.
2020-03-08Do not hardcode specific handling of Prop levels in template poly.Pierre-Marie Pédrot
We also factorize a few checks by returning an option when looking for a potentially template universe.
2020-03-08[doc] [dune] Update Dune build instructionsEmilio Jesus Gallego Arias
2020-03-08[exn] [nit] Remove not very useful re-raises.Emilio Jesus Gallego Arias
Cleanup: IMHO most of the re-raises here are not worth it.
2020-03-08Merge PR #11578: [exn] Keep information from multiple extra exn handlersPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-08Merge PR #11714: [gramlib] Refactor gramlib interface.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-08Merge PR #11740: Ltac2: Add notation for enough and eenoughPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-06Fix #11738 : Funind using deprecated Coqlib API.Pierre Courtieu
2020-03-06Merge PR #11698: Fix #11592: Side effect safety may be broken by universe ↵Gaëtan Gilbert
effects Reviewed-by: SkySkimmer
2020-03-06Merge PR #11723: Fix mishandling of sigma in guess_elim (regression from 8.11)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-06Merge PR #11717: [dune] [ocamldebug] Improve ocamldebug rulesGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-06Adding a test to the test-suite.Pierre-Marie Pédrot
We take inspiration and code from the Evil plugin.
2020-03-06Actually take advantage of the universes contained in side-effect certificates.Pierre-Marie Pédrot
2020-03-06Also check for monomorphic universes in side-effects certificates.Pierre-Marie Pédrot
2020-03-06Abstract away the API for side-effect certificates.Pierre-Marie Pédrot
2020-03-06Make explicit that the side-effect certificate trust is all-or-nothing.Pierre-Marie Pédrot
The current behaviour could be considered as sub-optimal, but it probably doesn't matter in practice as this happens when serializing side-effects.
2020-03-05Merge PR #11744: [dune] Fix bug in auto-configure deps.Théo Zimmermann
Reviewed-by: Zimmi48
2020-03-05Merge PR #11693: [boot] Don't initialize coqlib when `-boot` is passed.Enrico Tassi
Reviewed-by: gares
2020-03-05Merge PR #7791: Deprecating the declaration of arbitrary terms as hints.Maxime Dénès
Reviewed-by: Zimmi48 Reviewed-by: mattam82 Reviewed-by: maximedenes
2020-03-05Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ↵Pierre-Marie Pédrot
following the model of `pose (x:=t)`. Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-03-05Merge PR #11602: Adding support for an "only parsing" modifier in ↵Pierre-Marie Pédrot
"where"-based notation Reviewed-by: Zimmi48 Reviewed-by: maximedenes Reviewed-by: ppedrot
2020-03-04Merge PR #11715: Be robust in calculating visible ids for non-registered ↵Hugo Herbelin
constants. Reviewed-by: herbelin
2020-03-04[boot] Don't initialize coqlib when `-boot` is passed.Emilio Jesus Gallego Arias
We refactor handling of `-boot` so the "coqlib" guessing routine, `Envars.coqlib ()` is not called when bootstrapping. In compositional builds involving Coq's prelude we don't want for this guessing to happen, as the heuristics to locate the prelude will fail due to different build layout choices. Thus after this patch Coq does not do any guessing when `-boot` is passed, leaving the location of libraries to the usual command line parameters. Note that some other tooling still calls `Envars.coqlib`, however this should happen late enough as for it to be safe; we will fix that eventually when we consolidate the library for library handling among tools. Ideally, we would also remove `Envars.coqlib` altogether, as we want to avoid clients accessing the Coq filesystem in a non-controlled way.
2020-03-04Merge PR #11429: [zify] several efficiency enhancementsVincent Laporte
Reviewed-by: vbgl
2020-03-04Add overlay for equations.Hugo Herbelin
2020-03-04Experimenting using a record for decl_notation.Hugo Herbelin
2020-03-04Adding support for an "only parsing" modifier in "where"-based notations.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-03-04Merge PR #11380: [exninfo] Deprecate aliases for exception re-raising.Pierre-Marie Pédrot
Reviewed-by: Matafou Reviewed-by: ppedrot
2020-03-04Merge PR #11618: [loadpath] Rework and simplify ML loadpath handlingThéo Zimmermann
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: herbelin Reviewed-by: maximedenes
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:19:29 +0000