aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-12Documenting when exceptions are noncritical in the proof engineHugo Herbelin
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-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-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-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).
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:34:19 +0000