aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-04-13Close #11935: section variables do not have universe instances.Gaëtan Gilbert
2020-04-13Merge PR #11916: [proof] Introduce `prepare_proof` to improve normalization w...Gaëtan Gilbert
2020-04-13Merge PR #12081: [test-suite] Remove deprecated -I option of coqchk in MakefileGaëtan Gilbert
2020-04-13Merge PR #12087: Temporarily disable Windows job on Azure.Gaëtan Gilbert
2020-04-13Temporarily disable Windows job on Azure.Théo Zimmermann
2020-04-13Merge PR #11539: [dune] [stdlib] Build the standard library natively with Dune.Théo Zimmermann
2020-04-12[test-suite] Remove deprecated -I option of coqchk in MakefilePierre Roux
2020-04-11[dune] [doc] Remove the quick targets in favor of the shims.Emilio Jesus Gallego Arias
2020-04-11[dune] [stdlib] Build the standard library natively with Dune.Emilio Jesus Gallego Arias
2020-04-11[ci] [build] Bump Dune to 2.5.0Emilio Jesus Gallego Arias
2020-04-11Merge PR #11961: Convert vernac commands chapter to prodn, update syntaxThéo Zimmermann
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-04-10[sideeff] Don't use polymorphic equality to check for empty side-effectsEmilio Jesus Gallego Arias
2020-04-10[proof] Introduce `prepare_proof` to improve normalization workflow.Emilio Jesus Gallego Arias
2020-04-10Suppress the space after "#" when printing productionsJim Fehrle
2020-04-10Ignore subscripts in notation for matching cmds and tacsJim Fehrle
2020-04-10Fix prefix matchingJim Fehrle
2020-04-10Merge PR #12039: Do not erase native files in debug modePierre-Marie Pédrot
2020-04-10Merge PR #11882: Adding a short form of Ltac2 Fresh.freshPierre-Marie Pédrot
2020-04-10Merge PR #11756: [lib] Remove custom backtrace-destroying finalizersPierre-Marie Pédrot
2020-04-10Merge PR #12036: [ci] [fiat-crypto] [flambda] Don't use flambda for fiat-cryptoGaëtan Gilbert
2020-04-09Merge PR #12010: Remove dead code in Evarsolve alias algorithmHugo Herbelin
2020-04-09Code simplification in find_projectable_vars.Pierre-Marie Pédrot
2020-04-09Remove a unused computation in alias code.Pierre-Marie Pédrot
2020-04-09Inline an alias-computing function only used once.Pierre-Marie Pédrot
2020-04-09Remove dead code in Evarsolve alias resolution.Pierre-Marie Pédrot
2020-04-09Merge PR #12046: [errors] Print backtrace of internal errors in printersPierre-Marie Pédrot
2020-04-09Merge PR #11534: Support universe bindings and universe constraints in Let de...Gaëtan Gilbert
2020-04-09Merge PR #12056: [pre-commit] Check ocamlformat version and silence ocamlformat.Gaëtan Gilbert
2020-04-09Merge PR #12050: Fix a typo in CoqMakefile.inPierre-Marie Pédrot
2020-04-09[pre-commit] Check ocamlformat version and silence ocamlformat.Théo Zimmermann
2020-04-08Merge PR #12044: proposed fix for the issue #12015 (String_as_OT)Jason Gross
2020-04-08[ci] [fiat-crypto] [flambda] Don't use flambda for fiat-cryptoEmilio Jesus Gallego Arias
2020-04-08Merge PR #11909: Make the level of ≡ in Int63 consistent with =Hugo Herbelin
2020-04-08Fix a typo in CoqMakefile.inJason Gross
2020-04-08[errors] Print backtrace of internal errors in printersEmilio Jesus Gallego Arias
2020-04-08Merge PR #12005: Remove deprecated coqtop optionsEmilio Jesus Gallego Arias
2020-04-07Merge PR #11997: Clean and fix definitions of options.Emilio Jesus Gallego Arias
2020-04-07Integrated changes proposed by @JasonGrossilya
2020-04-07proposed fix for the issue #12015 (String_as_OT)ilya
2020-04-07Support universe bindings and universe constraints in Let definitions.Théo Zimmermann
2020-04-07Merge PR #12042: Fix documentation of Print Libraries following #10476.Clément Pit-Claudel
2020-04-07Fix documentation of Print Libraries following #10476.Théo Zimmermann
2020-04-07Do not erase native files in debug modeMaxime Dénès
2020-04-06Merge PR #12006: [coq_makefile] remove .lia.cache and .nia.cache by make clea...Enrico Tassi
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-04-06Merge PR #11955: Use the kernel machine in whd_betaiota_deltazeta_for_iota_stateMatthieu Sozeau
2020-04-05Merge PR #12025: Fixes #11194 (Canonical/Coercion not located for coqdoc)Emilio Jesus Gallego Arias
2020-04-05Fixes #11194 (Canonical/Coercion not located for coqdoc).Hugo Herbelin
2020-04-03Avoiding using a fixed introduction name in Ltac code of stdlib.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-22 12:30:47 +0000