aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2020-04-06Merge PR #12006: [coq_makefile] remove .lia.cache and .nia.cache by make clea...Enrico Tassi
2020-04-06Add overlays.Pierre-Marie Pédrot
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
2020-04-06Fix #11934 equality on constrexpr ignores instances of explicit applicationsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 23:54:37 +0000