aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-04-12Fixing export of CAML_LD_LIBRARY_PATH from config/Makefile to Makefile.common.Hugo Herbelin
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-11[gitlab-ci] Only run Windows jobs when ONLY_WINDOWS variable is true.Théo Zimmermann
2020-04-11Merge PR #11961: Convert vernac commands chapter to prodn, update syntaxThéo Zimmermann
2020-04-11add properties of operations on vectorsOlivier Laurent
2020-04-11Fix #7812Attila Gáspár
2020-04-11If a custom entry has global, a bound variable is valid in this entry.Hugo Herbelin
2020-04-11If a custom entry has global, an argument-free abbreviation is valid in this ...Hugo Herbelin
2020-04-11Renaming confusingly-named insert_coercion into insert_entry_coercion.Hugo Herbelin
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-04-10coqdoc: Report location of mismatched '[['Lysxia
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-10Change log for #12068 (Coqide segfault tentative fix).Hugo Herbelin
2020-04-10Coqide completion: Avoiding using an iterator in an apparently sensitive code.Hugo Herbelin
2020-04-10Merge PR #12036: [ci] [fiat-crypto] [flambda] Don't use flambda for fiat-cryptoGaëtan Gilbert
2020-04-10[obligations] Deprecated flag cleanupEmilio Jesus Gallego Arias
2020-04-10[ocamlformat] Enable for funind.Emilio Jesus Gallego Arias
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